1 files changed, 11 insertions, 44 deletions

diff --git a/hol-light/TacticRecording/xthm.ml b/hol-light/TacticRecording/xthm.ml
index 2619e03f..97fcec57 100644
--- a/hol-light/TacticRecording/xthm.ml
+++ b/hol-light/TacticRecording/xthm.ml
@@ -1,73 +1,40 @@
 
 
 
-(* ** DATATYPES ** *)
-
-
-type farg =
-   Fint of int
- | Fstring of string
- | Fterm of term
- | Ftype of hol_type
- | Fthm of finfo
- | Fpair of farg * farg
- | Flist of farg list
- | Ffn of finfo
-
-and finfo =
-   string option                     (* Function's name *)
- * farg list;;                       (* Function's args *)
-
-
-type label =
-   Tactical of finfo
- | Label of string;;
-
-
-(* Atomic tests *)
-
-let is_atomic_farg arg =
-  match arg with
-    Fthm (_,(_::_)) | Fpair _ -> false
-  | _ -> true;;
-
-let is_atomic_finfo ((x_,args):finfo) = (is_empty args);;
-
-
-(* active_info *)
-
-let active_info = (Some "...", []);;
+(* ** DATATYPE ** *)
 
 
 (* The 'xthm' datatype *)
 
-(* This couples a theorem with an 'finfo' representation of its proof.  For   *)
-(* named ML objects, this 'finfo' will simply be the ML name of the theorem.  *)
+(* This couples a theorem with an 'mldata' representation of its proof.  For  *)
+(* named ML objects, this 'mldata' will simply be the ML name of the theorem. *)
 (* For rule applications, it will capture the rule and its arguments.         *)
 
-type xthm = thm * finfo;;
+type xthm = thm * mldata;;
 
 type xconv = term -> xthm;;
 
 
 (* Constructors and destructors *)
 
-let mk_xthm (xth:thm*finfo) : xthm = xth;;
+let mk_xthm (xth:thm*mldata) : xthm = xth;;
 
-let mk_xthm0 x th = mk_xthm (th, (Some x, []));;
+let mk_xthm0 x th = mk_xthm (th, (x,[]));;
 
-let dest_xthm ((th,info):xthm) : thm * finfo = (th,info);;
+let dest_xthm ((th,prf):xthm) : thm * mldata = (th,prf);;
 
 let xthm_thm ((th,_):xthm) = th;;
 
-let xthm_proof ((_,info):xthm) = info;;
+let xthm_proof ((_,prf):xthm) = prf;;
+
+let name_xthm x ((th,_):xthm) : xthm = (th, (x,[]));;
 
 
 
 (* ** INSTALL PRINTERS ** *)
 
 
-let print_xthm ((th,info):xthm) = print_thm th;;
+let print_xthm ((th,_):xthm) = print_thm th;;
 
 #install_printer print_xthm;;