src/HOL/Import/proof_kernel.ML

     type hol_type
     type tag
     type term
     type thm
     type ('a,'b) subst
-	 
+
     type proof_info
     datatype proof = Proof of proof_info * proof_content
 	 and proof_content
 	   = PRefl of term
 	   | PInstT of proof * (hol_type,hol_type) subst

     val new_definition : string -> string -> term -> theory -> theory * thm
     val new_specification : string -> string -> string list -> thm -> theory -> theory * thm
     val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm
     val new_axiom : string -> term -> theory -> theory * thm
 
-    val prin : term -> unit 
-    val protect_factname : string -> string 
+    val prin : term -> unit
+    val protect_factname : string -> string
     val replay_protect_varname : string -> string -> unit
     val replay_add_dump : string -> theory -> theory
 end
 
 structure ProofKernel :> ProofKernel =

 type term = Term.term
 datatype tag = Tag of string list
 type ('a,'b) subst = ('a * 'b) list
 datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
 
-fun hthm2thm (HOLThm (_, th)) = th 
+fun hthm2thm (HOLThm (_, th)) = th
 
 fun to_hol_thm th = HOLThm ([], th)
 
 val replay_add_dump = add_dump
 fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
 
 datatype proof_info
   = Info of {disk_info: (string * string) option ref}
-	    
+
 datatype proof = Proof of proof_info * proof_content
      and proof_content
        = PRefl of term
        | PInstT of proof * (hol_type,hol_type) subst
        | PSubst of proof list * term * proof

        | PContr of proof * term
 
 exception PK of string * string
 fun ERR f mesg = PK (f,mesg)
 
-fun print_exn e = 
+fun print_exn e =
     case e of
 	PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
       | _ => OldGoals.print_exn e
 
 (* Compatibility. *)

 exception SMART_STRING
 
 fun smart_string_of_cterm ct =
     let
 	val {thy,t,T,...} = rep_cterm ct
+        val ctxt = ProofContext.init thy
         (* Hack to avoid parse errors with Trueprop *)
 	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
 		   handle TERM _ => ct)
-	fun match cu = t aconv (term_of cu)
+	fun match u = t aconv u
 	fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
 	  | G 1 = Library.setmp show_brackets true (G 0)
 	  | G 2 = Library.setmp show_all_types true (G 0)
 	  | G 3 = Library.setmp show_brackets true (G 2)
-          | G _ = raise SMART_STRING 
+          | G _ = raise SMART_STRING
 	fun F n =
 	    let
 		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
-		val cu  = Thm.read_cterm thy (str,T)
-	    in
-		if match cu
+		val u = Syntax.parse_term ctxt str
+                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
+	    in
+		if match u
 		then quote str
 		else F (n+1)
 	    end
 	    handle ERROR mesg => F (n+1)
 		 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
     in
       PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
     end
     handle ERROR mesg => simple_smart_string_of_cterm ct
- 
+
 val smart_string_of_thm = smart_string_of_cterm o cprop_of
 
 fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
 fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct)
 fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());

 			       then y
 			       else F rest
     in
 	F
     end
-fun i mem L = 
-    let fun itr [] = false 
-	  | itr (a::rst) = i=a orelse itr rst 
+fun i mem L =
+    let fun itr [] = false
+	  | itr (a::rst) = i=a orelse itr rst
     in itr L end;
-    
+
 fun insert i L = if i mem L then L else i::L
-					
+
 fun mk_set [] = []
   | mk_set (a::rst) = insert a (mk_set rst)
-		      
+
 fun [] union S = S
   | S union [] = S
   | (a::rst) union S2 = rst union (insert a S2)
-			
+
 fun implode_subst [] = []
   | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
   | implode_subst _ = raise ERR "implode_subst" "malformed substitution list"
 
 end

 val empty_tag = Tag []
 fun read name = Tag [name]
 fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2))
 end
 
-(* Acutal code. *)
+(* Actual code. *)
 
 fun get_segment thyname l = (Lib.assoc "s" l
 			     handle PK _ => thyname)
 val get_name : (string * string) list -> string = Lib.assoc "n"
 

 fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
   | dom_rng _ = raise ERR "dom_rng" "Not a functional type"
 
 fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
 
-local 
-  fun get_const sg thyname name = 
+local
+  fun get_const sg thyname name =
     (case Sign.const_type sg name of
       SOME ty => Const (name, ty)
     | NONE => raise ERR "get_type" (name ^ ": No such constant"))
 in
 fun prim_mk_const thy Thy Nam =

 fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
 
 val check_name_thy = theory "Main"
 
 fun valid_boundvarname s =
-  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
+  can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
 
 fun valid_varname s =
-  can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
+  can (fn () => Syntax.read_term_global check_name_thy s) ();
 
 fun protect_varname s =
     if innocent_varname s andalso valid_varname s then s else
     case Symtab.lookup (!protected_varnames) s of
       SOME t => t
-    | NONE => 
+    | NONE =>
       let
 	  val _ = inc invented_isavar
 	  val t = "u_" ^ string_of_int (!invented_isavar)
 	  val _ = ImportRecorder.protect_varname s t
           val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)

 	  t
       end
 
 exception REPLAY_PROTECT_VARNAME of string*string*string
 
-fun replay_protect_varname s t = 
+fun replay_protect_varname s t =
 	case Symtab.lookup (!protected_varnames) s of
 	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
-	| NONE => 	
+	| NONE =>
           let
 	      val _ = inc invented_isavar
 	      val t = "u_" ^ string_of_int (!invented_isavar)
               val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
           in
 	      ()
-          end	       	
-	 
+          end
+
 fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
 
 fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   | mk_lambda v t = raise TERM ("lambda", [v, t]);
- 
-fun replacestr x y s = 
+
+fun replacestr x y s =
 let
   val xl = explode x
   val yl = explode y
   fun isprefix [] ys = true
     | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
-    | isprefix _ _ = false  
+    | isprefix _ _ = false
   fun isp s = isprefix xl s
   fun chg s = yl@(List.drop (s, List.length xl))
   fun r [] = []
-    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) 
+    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
 in
   implode(r (explode s))
-end    
+end
 
 fun protect_factname s = replacestr "." "_dot_" s
-fun unprotect_factname s = replacestr "_dot_" "." s 
+fun unprotect_factname s = replacestr "_dot_" "." s
 
 val ty_num_prefix = "N_"
 
 fun startsWithDigit s = Char.isDigit (hd (String.explode s))
 
-fun protect_tyname tyn = 
+fun protect_tyname tyn =
   let
-    val tyn' = 
-      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else 
+    val tyn' =
+      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
       (if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
   in
     tyn'
   end
 
-fun protect_constname tcn = tcn 
+fun protect_constname tcn = tcn
  (* if tcn = ".." then "dotdot"
   else if tcn = "==" then "eqeq"
   else tcn*)
 
 structure TypeNet =

 		val f = get_term_from_index thy thyname types terms tmf
 		val a = get_term_from_index thy thyname types terms tma
 	    in
 		mk_comb(f,a)
 	    end
-	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 
-	    let		
-                val x = get_term_from_index thy thyname types terms tmx 
+	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
+	    let
+                val x = get_term_from_index thy thyname types terms tmx
                 val a = get_term_from_index thy thyname types terms tma
 	    in
 		mk_lambda x a
 	    end
 	  | gtfx (Elem("tmi",[("i",iS)],[])) =

 		 else find ps
 	     end) handle OS.SysErr _ => find ps
     in
 	Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
     end
-			   
+
 fun proof_file_name thyname thmname thy =
     let
 	val path = case get_proof_dir thyname thy of
 		       SOME p => p
 		     | NONE => error "Cannot find proof files"
 	val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
     in
 	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
     end
-	
+
 fun xml_to_proof thyname types terms prf thy =
     let
 	val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
 	val xml_to_term = TermNet.get_term_from_xml thy thyname types terms
 

 	  | x2p xml = raise ERR "x2p" "Bad proof"
     in
 	x2p prf
     end
 
-fun import_proof_concl thyname thmname thy = 
+fun import_proof_concl thyname thmname thy =
     let
 	val is = TextIO.openIn(proof_file_name thyname thmname thy)
 	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
 	val _ = TextIO.closeIn is
-    in 
+    in
 	case proof_xml of
 	    Elem("proof",[],xtypes::xterms::prf::rest) =>
 	    let
 		val types = TypeNet.input_types thyname xtypes
 		val terms = TermNet.input_terms thyname types xterms
-                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm               
+                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
 	    in
 		case rest of
 		    [] => NONE
 		  | [xtm] => SOME (f xtm)
 		  | _ => raise ERR "import_proof" "Bad argument list"

 fun import_proof thyname thmname thy =
     let
 	val is = TextIO.openIn(proof_file_name thyname thmname thy)
 	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
 	val _ = TextIO.closeIn is
-    in 
+    in
 	case proof_xml of
 	    Elem("proof",[],xtypes::xterms::prf::rest) =>
 	    let
 		val types = TypeNet.input_types thyname xtypes
 		val terms = TermNet.input_terms thyname types xterms

 	val res = implies_intr_hyps th4
     in
 	res
     end
 
-val permute_prems = Thm.permute_prems 
+val permute_prems = Thm.permute_prems
 
 fun rearrange sg tm th =
     let
 	val tm' = Envir.beta_eta_contract tm
 	fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)

       fun is_old_name n = n mem_string freenames
       fun name_of (Free (n, _)) = n
         | name_of _ = ERR "name_of"
       fun new_name' bump map n =
           let val n' = n^bump in
-            if is_old_name n' orelse Symtab.lookup map n' <> NONE then 
+            if is_old_name n' orelse Symtab.lookup map n' <> NONE then
               new_name' (Symbol.bump_string bump) map n
             else
               n'
-          end              
+          end
       val new_name = new_name' "a"
       fun replace_name n' (Free (n, t)) = Free (n', t)
         | replace_name n' _ = ERR "replace_name"
-      (* map: old or fresh name -> old free, 
+      (* map: old or fresh name -> old free,
          invmap: old free which has fresh name assigned to it -> fresh name *)
       fun dis (v, mapping as (map,invmap)) =
           let val n = name_of v in
             case Symtab.lookup map n of
               NONE => (Symtab.update (n, v) map, invmap)
-            | SOME v' => 
-              if v=v' then 
-                mapping 
+            | SOME v' =>
+              if v=v' then
+                mapping
               else
                 let val n' = new_name map n in
-                  (Symtab.update (n', v) map, 
+                  (Symtab.update (n', v) map,
                    Termtab.update (v, n') invmap)
                 end
           end
     in
       if (length freenames = length frees) then
         thm
       else
-        let 
-          val (_, invmap) = 
-              List.foldl dis (Symtab.empty, Termtab.empty) frees 
+        let
+          val (_, invmap) =
+              List.foldl dis (Symtab.empty, Termtab.empty) frees
           fun make_subst ((oldfree, newname), (intros, elims)) =
-              (cterm_of thy oldfree :: intros, 
+              (cterm_of thy oldfree :: intros,
                cterm_of thy (replace_name newname oldfree) :: elims)
           val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
-        in 
+        in
           forall_elim_list elims (forall_intr_list intros thm)
-        end     
+        end
     end
 
 val debug = ref false
 
 fun if_debug f x = if !debug then f x else ()

 val conjE_helper = permute_prems 0 1 conjE
 
 fun get_hol4_thm thyname thmname thy =
     case get_hol4_theorem thyname thmname thy of
 	SOME hth => SOME (HOLThm hth)
-      | NONE => 
+      | NONE =>
 	let
 	    val pending = HOL4Pending.get thy
 	in
 	    case StringPair.lookup pending (thyname,thmname) of
 		SOME hth => SOME (HOLThm hth)

 fun non_trivial_term_consts tm =
     List.filter (fn c => not (c = "Trueprop" orelse
 			 c = "All" orelse
 			 c = "op -->" orelse
 			 c = "op &" orelse
-			 c = "op =")) (Term.term_consts tm) 
+			 c = "op =")) (Term.term_consts tm)
 
 fun match_consts t (* th *) =
     let
 	fun add_consts (Const (c, _), cs) =
 	    (case c of

 		       | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping"))
 		  | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping")
 	    end
 	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
 	  | NONE =>
-	    let		
+	    let
 		val _ = (message "Looking for conclusion:";
 			 if_debug prin isaconc)
 		val cs = non_trivial_term_consts isaconc
 		val _ = (message "Looking for consts:";
 			 message (commas cs))

         let
 	    val (info,hol4conc') = disamb_term hol4conc
 	    val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
 	in
 	    case concl_of i2h_conc of
-		Const("==",_) $ lhs $ _ => 
+		Const("==",_) $ lhs $ _ =>
 		(warning ("Failed lookup of theorem '"^thmname^"':");
 	         writeln "Original conclusion:";
 		 prin hol4conc';
 		 writeln "Modified conclusion:";
 		 prin lhs)
 	      | _ => ()
 	end
   in
-      case b of 
+      case b of
 	  NONE => (warn () handle _ => (); (a,b))
 	| _ => (a, b)
-  end 
+  end
 
 fun get_thm thyname thmname thy =
     case get_hol4_thm thyname thmname thy of
 	SOME hth => (thy,SOME hth)
       | NONE => ((case import_proof_concl thyname thmname thy of

     let
 	val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
 	val rew = rewrite_hol4_term (concl_of th) thy
 	val th  = equal_elim rew th
 	val thy' = add_hol4_pending thyname thmname args thy
-	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') 
+	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
         val th = disambiguate_frees th
 	val thy2 = if gen_output
-		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ 
-                                  (smart_string_of_thm th) ^ "\n  by (import " ^ 
+		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
+                                  (smart_string_of_thm th) ^ "\n  by (import " ^
                                   thyname ^ " " ^ (quotename thmname) ^ ")") thy'
 		   else thy'
     in
 	(thy2,hth')
     end

 	val _ = message "RESULT:"
 	val _ = if_debug pth res
     in
 	(thy,res)
     end
-	
+
 
 fun CCONTR tm hth thy =
     let
 	val _ = message "SPEC:"
 	val _ = if_debug prin tm

 			      in
 				  mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
 			      end) th vlist'
 		end
 	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
-	      | NONE => 
+	      | NONE =>
 		foldr (fn (v,th) => mk_ABS v th thy) th vlist'
 	val res = HOLThm(rens_of info',th1)
 	val _ = message "RESULT:"
 	val _ = if_debug pth res
     in

 			    val p1 = quotename constname
 			    val p2 = string_of_ctyp (ctyp_of thy'' ctype)
 			    val p3 = string_of_mixfix csyn
 			    val p4 = smart_string_of_cterm crhs
 			in
-			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''  
+			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
 			end
 		    else
 			(add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
 				   "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
 				  thy'')
 	val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
 		      SOME (_,res) => HOLThm(rens_of linfo,res)
 		    | NONE => raise ERR "new_definition" "Bad conclusion"
 	val fullname = Sign.full_name thy22 thmname
 	val thy22' = case opt_get_output_thy thy22 of
-			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; 
+			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
 				add_hol4_mapping thyname thmname fullname thy22)
 		       | output_thy =>
 			 let
 			     val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
 			     val _ = ImportRecorder.add_hol_move fullname moved_thmname

     val helper = thm "termspec_help"
 in
 fun new_specification thyname thmname names hth thy =
     case HOL4DefThy.get thy of
 	Replaying _ => (thy,hth)
-      | _ => 
+      | _ =>
 	let
 	    val _ = message "NEW_SPEC:"
 	    val _ = if_debug pth hth
 	    val names = map (rename_const thyname thy) names
 	    val _ = warning ("Introducing constants " ^ commas names)

 				   handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
 			       fun dest_exists (Const("Ex",_) $ abody) =
 				   dest_eta_abs abody
 				 | dest_exists tm =
 				   raise ERR "new_specification" "Bad existential formula"
-					 
+
 			       val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
 							  let
 							      val (_,cT,p) = dest_exists ex
 							  in
 							      ((cname,cT,mk_syn thy cname)::cs,p)

 	    val _ = if_debug pth hth
 	in
 	    intern_store_thm false thyname thmname hth thy''
 	end
 	handle e => (message "exception in new_specification"; print_exn e)
-		    
+
 end
-			   
+
 fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
-				      
+
 fun to_isa_thm (hth as HOLThm(_,th)) =
     let
 	val (HOLThm args) = norm_hthm (theory_of_thm th) hth
     in
 	apsnd strip_shyps args

     val typedef_hol2hollight = thm "typedef_hol2hollight"
 in
 fun new_type_definition thyname thmname tycname hth thy =
     case HOL4DefThy.get thy of
 	Replaying _ => (thy,hth)
-      | _ => 
+      | _ =>
 	let
 	    val _ = message "TYPE_DEF:"
 	    val _ = if_debug pth hth
 	    val _ = warning ("Introducing type " ^ tycname)
 	    val (HOLThm(rens,td_th)) = norm_hthm thy hth

 		      | _ => raise ERR "new_type_definition" "Bad type definition theorem"
 	    val tfrees = term_tfrees c
 	    val tnames = map fst tfrees
 	    val tsyn = mk_syn thy tycname
 	    val typ = (tycname,tnames,tsyn)
-	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
+	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
-				      
+
 	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
 
 	    val fulltyname = Sign.intern_type thy' tycname
 	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
 	    val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname

 				then ""
 				else "(" ^ commas tnames ^ ") "
 	    val proc_prop = if null tnames
 			    then smart_string_of_cterm
 			    else Library.setmp show_all_types true smart_string_of_cterm
-	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " 
+	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
 				 ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
-	    
+
 	    val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
-              
+
 	    val _ = message "RESULT:"
 	    val _ = if_debug pth hth'
 	in
 	    (thy6,hth')
 	end

 	val syn = string_of_mixfix (mk_syn thy constname)
 	(*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
         val eq = quote (constname ^ " == "^rhs)
 	val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
     in
-	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy    
-    end
-
-fun add_dump_syntax thy name = 
+	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy
+    end
+
+fun add_dump_syntax thy name =
     let
       val n = quotename name
       val syn = string_of_mixfix (mk_syn thy name)
     in
       add_dump ("syntax\n  "^n^" :: _ "^syn) thy
     end
-      
+
 (*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
-fun choose_upon_replay_history thy s dth = 
+fun choose_upon_replay_history thy s dth =
     case Symtab.lookup (!type_intro_replay_history) s of
 	NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
       | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
 *)
 
 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
     case HOL4DefThy.get thy of
 	Replaying _ => (thy,
           HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
-      | _ => 
+      | _ =>
 	let
             val _ = message "TYPE_INTRO:"
 	    val _ = if_debug pth hth
 	    val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
 	    val (HOLThm(rens,td_th)) = norm_hthm thy hth

 	    val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
 	    val fulltyname = Sign.intern_type thy' tycname
 	    val aty = Type (fulltyname, map mk_vartype tnames)
 	    val abs_ty = tT --> aty
 	    val rep_ty = aty --> tT
-            val typedef_hol2hollight' = 
-		Drule.instantiate' 
-		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] 
+            val typedef_hol2hollight' =
+		Drule.instantiate'
+		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
 		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
                     typedef_hol2hollight
 	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
             val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
               raise ERR "type_introduction" "no type variables expected any more"

 	    val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
             val _ = message "step 4"
 	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
 	    val thy4 = add_hol4_pending thyname thmname args thy''
 	    val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
-	   
+
 	    val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
 	    val c   =
 		let
 		    val PT = type_of P'
 		in
 		    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
 		end
-	    
+
 	    val tnames_string = if null tnames
 				then ""
 				else "(" ^ commas tnames ^ ") "
 	    val proc_prop = if null tnames
 			    then smart_string_of_cterm
 			    else Library.setmp show_all_types true smart_string_of_cterm
-	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ 
-              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ 
+	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
+              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
 	      (string_of_mixfix tsyn) ^ " morphisms "^
-              (quote rep_name)^" "^(quote abs_name)^"\n"^ 
+              (quote rep_name)^" "^(quote abs_name)^"\n"^
 	      ("  apply (rule light_ex_imp_nonempty[where t="^
-              (proc_prop (cterm_of thy4 t))^"])\n"^              
+              (proc_prop (cterm_of thy4 t))^"])\n"^
 	      ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
 	    val str_aty = string_of_ctyp (ctyp_of thy aty)
-            val thy = add_dump_syntax thy rep_name 
+            val thy = add_dump_syntax thy rep_name
             val thy = add_dump_syntax thy abs_name
-	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ 
+	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
               " = typedef_hol2hollight \n"^
               "  [where a=\"a :: "^str_aty^"\" and r=r" ^
-	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy 
+	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
 	    val _ = message "RESULT:"
 	    val _ = if_debug pth hth'
 	in
 	    (thy,hth')
 	end