src/HOL/Import/proof_kernel.ML
changeset 24707 dfeb98f84e93
parent 24634 38db11874724
child 24712 64ed05609568
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 25 13:28:35 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 25 13:28:37 2007 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4      type term
     1.5      type thm
     1.6      type ('a,'b) subst
     1.7 -	 
     1.8 +
     1.9      type proof_info
    1.10      datatype proof = Proof of proof_info * proof_content
    1.11  	 and proof_content
    1.12 @@ -111,8 +111,8 @@
    1.13      val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm
    1.14      val new_axiom : string -> term -> theory -> theory * thm
    1.15  
    1.16 -    val prin : term -> unit 
    1.17 -    val protect_factname : string -> string 
    1.18 +    val prin : term -> unit
    1.19 +    val protect_factname : string -> string
    1.20      val replay_protect_varname : string -> string -> unit
    1.21      val replay_add_dump : string -> theory -> theory
    1.22  end
    1.23 @@ -125,7 +125,7 @@
    1.24  type ('a,'b) subst = ('a * 'b) list
    1.25  datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
    1.26  
    1.27 -fun hthm2thm (HOLThm (_, th)) = th 
    1.28 +fun hthm2thm (HOLThm (_, th)) = th
    1.29  
    1.30  fun to_hol_thm th = HOLThm ([], th)
    1.31  
    1.32 @@ -134,7 +134,7 @@
    1.33  
    1.34  datatype proof_info
    1.35    = Info of {disk_info: (string * string) option ref}
    1.36 -	    
    1.37 +
    1.38  datatype proof = Proof of proof_info * proof_content
    1.39       and proof_content
    1.40         = PRefl of term
    1.41 @@ -176,7 +176,7 @@
    1.42  exception PK of string * string
    1.43  fun ERR f mesg = PK (f,mesg)
    1.44  
    1.45 -fun print_exn e = 
    1.46 +fun print_exn e =
    1.47      case e of
    1.48  	PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
    1.49        | _ => OldGoals.print_exn e
    1.50 @@ -213,21 +213,23 @@
    1.51  fun smart_string_of_cterm ct =
    1.52      let
    1.53  	val {thy,t,T,...} = rep_cterm ct
    1.54 +        val ctxt = ProofContext.init thy
    1.55          (* Hack to avoid parse errors with Trueprop *)
    1.56  	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    1.57  		   handle TERM _ => ct)
    1.58 -	fun match cu = t aconv (term_of cu)
    1.59 +	fun match u = t aconv u
    1.60  	fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
    1.61  	  | G 1 = Library.setmp show_brackets true (G 0)
    1.62  	  | G 2 = Library.setmp show_all_types true (G 0)
    1.63  	  | G 3 = Library.setmp show_brackets true (G 2)
    1.64 -          | G _ = raise SMART_STRING 
    1.65 +          | G _ = raise SMART_STRING
    1.66  	fun F n =
    1.67  	    let
    1.68  		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    1.69 -		val cu  = Thm.read_cterm thy (str,T)
    1.70 +		val u = Syntax.parse_term ctxt str
    1.71 +                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
    1.72  	    in
    1.73 -		if match cu
    1.74 +		if match u
    1.75  		then quote str
    1.76  		else F (n+1)
    1.77  	    end
    1.78 @@ -237,7 +239,7 @@
    1.79        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    1.80      end
    1.81      handle ERROR mesg => simple_smart_string_of_cterm ct
    1.82 - 
    1.83 +
    1.84  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    1.85  
    1.86  fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
    1.87 @@ -272,20 +274,20 @@
    1.88      in
    1.89  	F
    1.90      end
    1.91 -fun i mem L = 
    1.92 -    let fun itr [] = false 
    1.93 -	  | itr (a::rst) = i=a orelse itr rst 
    1.94 +fun i mem L =
    1.95 +    let fun itr [] = false
    1.96 +	  | itr (a::rst) = i=a orelse itr rst
    1.97      in itr L end;
    1.98 -    
    1.99 +
   1.100  fun insert i L = if i mem L then L else i::L
   1.101 -					
   1.102 +
   1.103  fun mk_set [] = []
   1.104    | mk_set (a::rst) = insert a (mk_set rst)
   1.105 -		      
   1.106 +
   1.107  fun [] union S = S
   1.108    | S union [] = S
   1.109    | (a::rst) union S2 = rst union (insert a S2)
   1.110 -			
   1.111 +
   1.112  fun implode_subst [] = []
   1.113    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
   1.114    | implode_subst _ = raise ERR "implode_subst" "malformed substitution list"
   1.115 @@ -300,7 +302,7 @@
   1.116  fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2))
   1.117  end
   1.118  
   1.119 -(* Acutal code. *)
   1.120 +(* Actual code. *)
   1.121  
   1.122  fun get_segment thyname l = (Lib.assoc "s" l
   1.123  			     handle PK _ => thyname)
   1.124 @@ -430,8 +432,8 @@
   1.125  
   1.126  fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
   1.127  
   1.128 -local 
   1.129 -  fun get_const sg thyname name = 
   1.130 +local
   1.131 +  fun get_const sg thyname name =
   1.132      (case Sign.const_type sg name of
   1.133        SOME ty => Const (name, ty)
   1.134      | NONE => raise ERR "get_type" (name ^ ": No such constant"))
   1.135 @@ -472,16 +474,16 @@
   1.136  val check_name_thy = theory "Main"
   1.137  
   1.138  fun valid_boundvarname s =
   1.139 -  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
   1.140 +  can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
   1.141  
   1.142  fun valid_varname s =
   1.143 -  can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
   1.144 +  can (fn () => Syntax.read_term_global check_name_thy s) ();
   1.145  
   1.146  fun protect_varname s =
   1.147      if innocent_varname s andalso valid_varname s then s else
   1.148      case Symtab.lookup (!protected_varnames) s of
   1.149        SOME t => t
   1.150 -    | NONE => 
   1.151 +    | NONE =>
   1.152        let
   1.153  	  val _ = inc invented_isavar
   1.154  	  val t = "u_" ^ string_of_int (!invented_isavar)
   1.155 @@ -493,56 +495,56 @@
   1.156  
   1.157  exception REPLAY_PROTECT_VARNAME of string*string*string
   1.158  
   1.159 -fun replay_protect_varname s t = 
   1.160 +fun replay_protect_varname s t =
   1.161  	case Symtab.lookup (!protected_varnames) s of
   1.162  	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
   1.163 -	| NONE => 	
   1.164 +	| NONE =>
   1.165            let
   1.166  	      val _ = inc invented_isavar
   1.167  	      val t = "u_" ^ string_of_int (!invented_isavar)
   1.168                val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   1.169            in
   1.170  	      ()
   1.171 -          end	       	
   1.172 -	 
   1.173 +          end
   1.174 +
   1.175  fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
   1.176  
   1.177  fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   1.178    | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   1.179    | mk_lambda v t = raise TERM ("lambda", [v, t]);
   1.180 - 
   1.181 -fun replacestr x y s = 
   1.182 +
   1.183 +fun replacestr x y s =
   1.184  let
   1.185    val xl = explode x
   1.186    val yl = explode y
   1.187    fun isprefix [] ys = true
   1.188      | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
   1.189 -    | isprefix _ _ = false  
   1.190 +    | isprefix _ _ = false
   1.191    fun isp s = isprefix xl s
   1.192    fun chg s = yl@(List.drop (s, List.length xl))
   1.193    fun r [] = []
   1.194 -    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) 
   1.195 +    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
   1.196  in
   1.197    implode(r (explode s))
   1.198 -end    
   1.199 +end
   1.200  
   1.201  fun protect_factname s = replacestr "." "_dot_" s
   1.202 -fun unprotect_factname s = replacestr "_dot_" "." s 
   1.203 +fun unprotect_factname s = replacestr "_dot_" "." s
   1.204  
   1.205  val ty_num_prefix = "N_"
   1.206  
   1.207  fun startsWithDigit s = Char.isDigit (hd (String.explode s))
   1.208  
   1.209 -fun protect_tyname tyn = 
   1.210 +fun protect_tyname tyn =
   1.211    let
   1.212 -    val tyn' = 
   1.213 -      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else 
   1.214 +    val tyn' =
   1.215 +      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
   1.216        (if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
   1.217    in
   1.218      tyn'
   1.219    end
   1.220  
   1.221 -fun protect_constname tcn = tcn 
   1.222 +fun protect_constname tcn = tcn
   1.223   (* if tcn = ".." then "dotdot"
   1.224    else if tcn = "==" then "eqeq"
   1.225    else tcn*)
   1.226 @@ -634,9 +636,9 @@
   1.227  	    in
   1.228  		mk_comb(f,a)
   1.229  	    end
   1.230 -	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 
   1.231 -	    let		
   1.232 -                val x = get_term_from_index thy thyname types terms tmx 
   1.233 +	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
   1.234 +	    let
   1.235 +                val x = get_term_from_index thy thyname types terms tmx
   1.236                  val a = get_term_from_index thy thyname types terms tma
   1.237  	    in
   1.238  		mk_lambda x a
   1.239 @@ -683,7 +685,7 @@
   1.240      in
   1.241  	Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
   1.242      end
   1.243 -			   
   1.244 +
   1.245  fun proof_file_name thyname thmname thy =
   1.246      let
   1.247  	val path = case get_proof_dir thyname thy of
   1.248 @@ -693,7 +695,7 @@
   1.249      in
   1.250  	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
   1.251      end
   1.252 -	
   1.253 +
   1.254  fun xml_to_proof thyname types terms prf thy =
   1.255      let
   1.256  	val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
   1.257 @@ -936,18 +938,18 @@
   1.258  	x2p prf
   1.259      end
   1.260  
   1.261 -fun import_proof_concl thyname thmname thy = 
   1.262 +fun import_proof_concl thyname thmname thy =
   1.263      let
   1.264  	val is = TextIO.openIn(proof_file_name thyname thmname thy)
   1.265  	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   1.266  	val _ = TextIO.closeIn is
   1.267 -    in 
   1.268 +    in
   1.269  	case proof_xml of
   1.270  	    Elem("proof",[],xtypes::xterms::prf::rest) =>
   1.271  	    let
   1.272  		val types = TypeNet.input_types thyname xtypes
   1.273  		val terms = TermNet.input_terms thyname types xterms
   1.274 -                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm               
   1.275 +                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
   1.276  	    in
   1.277  		case rest of
   1.278  		    [] => NONE
   1.279 @@ -962,7 +964,7 @@
   1.280  	val is = TextIO.openIn(proof_file_name thyname thmname thy)
   1.281  	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   1.282  	val _ = TextIO.closeIn is
   1.283 -    in 
   1.284 +    in
   1.285  	case proof_xml of
   1.286  	    Elem("proof",[],xtypes::xterms::prf::rest) =>
   1.287  	    let
   1.288 @@ -1068,7 +1070,7 @@
   1.289  	res
   1.290      end
   1.291  
   1.292 -val permute_prems = Thm.permute_prems 
   1.293 +val permute_prems = Thm.permute_prems
   1.294  
   1.295  fun rearrange sg tm th =
   1.296      let
   1.297 @@ -1152,26 +1154,26 @@
   1.298          | name_of _ = ERR "name_of"
   1.299        fun new_name' bump map n =
   1.300            let val n' = n^bump in
   1.301 -            if is_old_name n' orelse Symtab.lookup map n' <> NONE then 
   1.302 +            if is_old_name n' orelse Symtab.lookup map n' <> NONE then
   1.303                new_name' (Symbol.bump_string bump) map n
   1.304              else
   1.305                n'
   1.306 -          end              
   1.307 +          end
   1.308        val new_name = new_name' "a"
   1.309        fun replace_name n' (Free (n, t)) = Free (n', t)
   1.310          | replace_name n' _ = ERR "replace_name"
   1.311 -      (* map: old or fresh name -> old free, 
   1.312 +      (* map: old or fresh name -> old free,
   1.313           invmap: old free which has fresh name assigned to it -> fresh name *)
   1.314        fun dis (v, mapping as (map,invmap)) =
   1.315            let val n = name_of v in
   1.316              case Symtab.lookup map n of
   1.317                NONE => (Symtab.update (n, v) map, invmap)
   1.318 -            | SOME v' => 
   1.319 -              if v=v' then 
   1.320 -                mapping 
   1.321 +            | SOME v' =>
   1.322 +              if v=v' then
   1.323 +                mapping
   1.324                else
   1.325                  let val n' = new_name map n in
   1.326 -                  (Symtab.update (n', v) map, 
   1.327 +                  (Symtab.update (n', v) map,
   1.328                     Termtab.update (v, n') invmap)
   1.329                  end
   1.330            end
   1.331 @@ -1179,16 +1181,16 @@
   1.332        if (length freenames = length frees) then
   1.333          thm
   1.334        else
   1.335 -        let 
   1.336 -          val (_, invmap) = 
   1.337 -              List.foldl dis (Symtab.empty, Termtab.empty) frees 
   1.338 +        let
   1.339 +          val (_, invmap) =
   1.340 +              List.foldl dis (Symtab.empty, Termtab.empty) frees
   1.341            fun make_subst ((oldfree, newname), (intros, elims)) =
   1.342 -              (cterm_of thy oldfree :: intros, 
   1.343 +              (cterm_of thy oldfree :: intros,
   1.344                 cterm_of thy (replace_name newname oldfree) :: elims)
   1.345            val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
   1.346 -        in 
   1.347 +        in
   1.348            forall_elim_list elims (forall_intr_list intros thm)
   1.349 -        end     
   1.350 +        end
   1.351      end
   1.352  
   1.353  val debug = ref false
   1.354 @@ -1201,7 +1203,7 @@
   1.355  fun get_hol4_thm thyname thmname thy =
   1.356      case get_hol4_theorem thyname thmname thy of
   1.357  	SOME hth => SOME (HOLThm hth)
   1.358 -      | NONE => 
   1.359 +      | NONE =>
   1.360  	let
   1.361  	    val pending = HOL4Pending.get thy
   1.362  	in
   1.363 @@ -1215,7 +1217,7 @@
   1.364  			 c = "All" orelse
   1.365  			 c = "op -->" orelse
   1.366  			 c = "op &" orelse
   1.367 -			 c = "op =")) (Term.term_consts tm) 
   1.368 +			 c = "op =")) (Term.term_consts tm)
   1.369  
   1.370  fun match_consts t (* th *) =
   1.371      let
   1.372 @@ -1291,7 +1293,7 @@
   1.373  	    end
   1.374  	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
   1.375  	  | NONE =>
   1.376 -	    let		
   1.377 +	    let
   1.378  		val _ = (message "Looking for conclusion:";
   1.379  			 if_debug prin isaconc)
   1.380  		val cs = non_trivial_term_consts isaconc
   1.381 @@ -1325,7 +1327,7 @@
   1.382  	    val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
   1.383  	in
   1.384  	    case concl_of i2h_conc of
   1.385 -		Const("==",_) $ lhs $ _ => 
   1.386 +		Const("==",_) $ lhs $ _ =>
   1.387  		(warning ("Failed lookup of theorem '"^thmname^"':");
   1.388  	         writeln "Original conclusion:";
   1.389  		 prin hol4conc';
   1.390 @@ -1334,10 +1336,10 @@
   1.391  	      | _ => ()
   1.392  	end
   1.393    in
   1.394 -      case b of 
   1.395 +      case b of
   1.396  	  NONE => (warn () handle _ => (); (a,b))
   1.397  	| _ => (a, b)
   1.398 -  end 
   1.399 +  end
   1.400  
   1.401  fun get_thm thyname thmname thy =
   1.402      case get_hol4_thm thyname thmname thy of
   1.403 @@ -1373,11 +1375,11 @@
   1.404  	val rew = rewrite_hol4_term (concl_of th) thy
   1.405  	val th  = equal_elim rew th
   1.406  	val thy' = add_hol4_pending thyname thmname args thy
   1.407 -	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') 
   1.408 +	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   1.409          val th = disambiguate_frees th
   1.410  	val thy2 = if gen_output
   1.411 -		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ 
   1.412 -                                  (smart_string_of_thm th) ^ "\n  by (import " ^ 
   1.413 +		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
   1.414 +                                  (smart_string_of_thm th) ^ "\n  by (import " ^
   1.415                                    thyname ^ " " ^ (quotename thmname) ^ ")") thy'
   1.416  		   else thy'
   1.417      in
   1.418 @@ -1768,7 +1770,7 @@
   1.419      in
   1.420  	(thy,res)
   1.421      end
   1.422 -	
   1.423 +
   1.424  
   1.425  fun CCONTR tm hth thy =
   1.426      let
   1.427 @@ -1851,7 +1853,7 @@
   1.428  			      end) th vlist'
   1.429  		end
   1.430  	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
   1.431 -	      | NONE => 
   1.432 +	      | NONE =>
   1.433  		foldr (fn (v,th) => mk_ABS v th thy) th vlist'
   1.434  	val res = HOLThm(rens_of info',th1)
   1.435  	val _ = message "RESULT:"
   1.436 @@ -1947,7 +1949,7 @@
   1.437  			    val p3 = string_of_mixfix csyn
   1.438  			    val p4 = smart_string_of_cterm crhs
   1.439  			in
   1.440 -			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''  
   1.441 +			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
   1.442  			end
   1.443  		    else
   1.444  			(add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
   1.445 @@ -1958,7 +1960,7 @@
   1.446  		    | NONE => raise ERR "new_definition" "Bad conclusion"
   1.447  	val fullname = Sign.full_name thy22 thmname
   1.448  	val thy22' = case opt_get_output_thy thy22 of
   1.449 -			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; 
   1.450 +			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
   1.451  				add_hol4_mapping thyname thmname fullname thy22)
   1.452  		       | output_thy =>
   1.453  			 let
   1.454 @@ -1982,7 +1984,7 @@
   1.455  fun new_specification thyname thmname names hth thy =
   1.456      case HOL4DefThy.get thy of
   1.457  	Replaying _ => (thy,hth)
   1.458 -      | _ => 
   1.459 +      | _ =>
   1.460  	let
   1.461  	    val _ = message "NEW_SPEC:"
   1.462  	    val _ = if_debug pth hth
   1.463 @@ -2005,7 +2007,7 @@
   1.464  				   dest_eta_abs abody
   1.465  				 | dest_exists tm =
   1.466  				   raise ERR "new_specification" "Bad existential formula"
   1.467 -					 
   1.468 +
   1.469  			       val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
   1.470  							  let
   1.471  							      val (_,cT,p) = dest_exists ex
   1.472 @@ -2056,11 +2058,11 @@
   1.473  	    intern_store_thm false thyname thmname hth thy''
   1.474  	end
   1.475  	handle e => (message "exception in new_specification"; print_exn e)
   1.476 -		    
   1.477 +
   1.478  end
   1.479 -			   
   1.480 +
   1.481  fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
   1.482 -				      
   1.483 +
   1.484  fun to_isa_thm (hth as HOLThm(_,th)) =
   1.485      let
   1.486  	val (HOLThm args) = norm_hthm (theory_of_thm th) hth
   1.487 @@ -2079,7 +2081,7 @@
   1.488  fun new_type_definition thyname thmname tycname hth thy =
   1.489      case HOL4DefThy.get thy of
   1.490  	Replaying _ => (thy,hth)
   1.491 -      | _ => 
   1.492 +      | _ =>
   1.493  	let
   1.494  	    val _ = message "TYPE_DEF:"
   1.495  	    val _ = if_debug pth hth
   1.496 @@ -2093,9 +2095,9 @@
   1.497  	    val tnames = map fst tfrees
   1.498  	    val tsyn = mk_syn thy tycname
   1.499  	    val typ = (tycname,tnames,tsyn)
   1.500 -	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
   1.501 +	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
   1.502              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
   1.503 -				      
   1.504 +
   1.505  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
   1.506  
   1.507  	    val fulltyname = Sign.intern_type thy' tycname
   1.508 @@ -2124,11 +2126,11 @@
   1.509  	    val proc_prop = if null tnames
   1.510  			    then smart_string_of_cterm
   1.511  			    else Library.setmp show_all_types true smart_string_of_cterm
   1.512 -	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " 
   1.513 +	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
   1.514  				 ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
   1.515 -	    
   1.516 +
   1.517  	    val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
   1.518 -              
   1.519 +
   1.520  	    val _ = message "RESULT:"
   1.521  	    val _ = if_debug pth hth'
   1.522  	in
   1.523 @@ -2145,19 +2147,19 @@
   1.524          val eq = quote (constname ^ " == "^rhs)
   1.525  	val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
   1.526      in
   1.527 -	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy    
   1.528 +	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy
   1.529      end
   1.530  
   1.531 -fun add_dump_syntax thy name = 
   1.532 +fun add_dump_syntax thy name =
   1.533      let
   1.534        val n = quotename name
   1.535        val syn = string_of_mixfix (mk_syn thy name)
   1.536      in
   1.537        add_dump ("syntax\n  "^n^" :: _ "^syn) thy
   1.538      end
   1.539 -      
   1.540 +
   1.541  (*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
   1.542 -fun choose_upon_replay_history thy s dth = 
   1.543 +fun choose_upon_replay_history thy s dth =
   1.544      case Symtab.lookup (!type_intro_replay_history) s of
   1.545  	NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
   1.546        | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
   1.547 @@ -2167,7 +2169,7 @@
   1.548      case HOL4DefThy.get thy of
   1.549  	Replaying _ => (thy,
   1.550            HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
   1.551 -      | _ => 
   1.552 +      | _ =>
   1.553  	let
   1.554              val _ = message "TYPE_INTRO:"
   1.555  	    val _ = if_debug pth hth
   1.556 @@ -2192,9 +2194,9 @@
   1.557  	    val aty = Type (fulltyname, map mk_vartype tnames)
   1.558  	    val abs_ty = tT --> aty
   1.559  	    val rep_ty = aty --> tT
   1.560 -            val typedef_hol2hollight' = 
   1.561 -		Drule.instantiate' 
   1.562 -		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] 
   1.563 +            val typedef_hol2hollight' =
   1.564 +		Drule.instantiate'
   1.565 +		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
   1.566  		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
   1.567                      typedef_hol2hollight
   1.568  	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
   1.569 @@ -2209,7 +2211,7 @@
   1.570  	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
   1.571  	    val thy4 = add_hol4_pending thyname thmname args thy''
   1.572  	    val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   1.573 -	   
   1.574 +
   1.575  	    val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
   1.576  	    val c   =
   1.577  		let
   1.578 @@ -2217,27 +2219,27 @@
   1.579  		in
   1.580  		    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
   1.581  		end
   1.582 -	    
   1.583 +
   1.584  	    val tnames_string = if null tnames
   1.585  				then ""
   1.586  				else "(" ^ commas tnames ^ ") "
   1.587  	    val proc_prop = if null tnames
   1.588  			    then smart_string_of_cterm
   1.589  			    else Library.setmp show_all_types true smart_string_of_cterm
   1.590 -	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ 
   1.591 -              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ 
   1.592 +	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
   1.593 +              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
   1.594  	      (string_of_mixfix tsyn) ^ " morphisms "^
   1.595 -              (quote rep_name)^" "^(quote abs_name)^"\n"^ 
   1.596 +              (quote rep_name)^" "^(quote abs_name)^"\n"^
   1.597  	      ("  apply (rule light_ex_imp_nonempty[where t="^
   1.598 -              (proc_prop (cterm_of thy4 t))^"])\n"^              
   1.599 +              (proc_prop (cterm_of thy4 t))^"])\n"^
   1.600  	      ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
   1.601  	    val str_aty = string_of_ctyp (ctyp_of thy aty)
   1.602 -            val thy = add_dump_syntax thy rep_name 
   1.603 +            val thy = add_dump_syntax thy rep_name
   1.604              val thy = add_dump_syntax thy abs_name
   1.605 -	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ 
   1.606 +	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
   1.607                " = typedef_hol2hollight \n"^
   1.608                "  [where a=\"a :: "^str_aty^"\" and r=r" ^
   1.609 -	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy 
   1.610 +	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
   1.611  	    val _ = message "RESULT:"
   1.612  	    val _ = if_debug pth hth'
   1.613  	in