# HG changeset patch
# User skalberg
# Date 1081085654 -7200
# Node ID c3019a66180f2b5016b645b3811ad903f687215a
# Parent  7ae3b247c6e90dd5775d712d111db4d450b4b236
Added a number of explicit type casts and delayed evaluations (all seemingly
needless) so that SML/NJ 110.9.1 would accept the importer...

diff -r 7ae3b247c6e9 -r c3019a66180f src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Fri Apr 02 17:40:32 2004 +0200
+++ b/src/HOL/Import/hol4rews.ML	Sun Apr 04 15:34:14 2004 +0200
@@ -81,7 +81,7 @@
 val empty = Symtab.empty
 val copy = I
 val prep_ext = I
-val merge = Symtab.merge (K true)
+val merge : T * T -> T = Symtab.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 moves:"
 	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
@@ -96,7 +96,7 @@
 val empty = Symtab.empty
 val copy = I
 val prep_ext = I
-val merge = Symtab.merge (K true)
+val merge : T * T -> T = Symtab.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 imports:"
 	(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))
@@ -126,7 +126,7 @@
 val empty = Symtab.empty
 val copy = I
 val prep_ext = I
-val merge = Symtab.merge (K true)
+val merge : T * T -> T = Symtab.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
 	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
@@ -141,7 +141,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 mappings:"
 	(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of Some th => " --> " ^ th | None => "IGNORED"))::xl)) ([],tab)))
@@ -156,7 +156,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 mappings:"
 	(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))
@@ -171,7 +171,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
 	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
@@ -186,7 +186,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
 	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))
@@ -201,7 +201,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
 	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))
@@ -216,7 +216,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
 	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
@@ -231,7 +231,7 @@
 val empty = StringPair.empty
 val copy = I
 val prep_ext = I
-val merge = StringPair.merge (K true)
+val merge : T * T -> T = StringPair.merge (K true)
 fun print sg tab =
     Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
 	(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))
@@ -736,6 +736,7 @@
       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
       | handle_meta [x] = Appl[Constant "Trueprop",x]
+      | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
 in
 val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
 end
diff -r 7ae3b247c6e9 -r c3019a66180f src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Fri Apr 02 17:40:32 2004 +0200
+++ b/src/HOL/Import/import_syntax.ML	Sun Apr 04 15:34:14 2004 +0200
@@ -37,24 +37,25 @@
 				      |> Theory.add_path thyname
 				      |> add_dump (";setup_theory " ^ thyname))
 
-val end_import = Scan.succeed
-		     (fn thy =>
-			 let
-			     val thyname = get_generating_thy thy
-			     val segname = get_import_segment thy
-			     val (int_thms,facts) = Replay.setup_int_thms thyname thy
-			     val thmnames = filter (not o should_ignore thyname thy) facts
-			 in
-			     thy |> clear_import_thy
-				 |> set_segment thyname segname
-				 |> set_used_names facts
-				 |> Replay.import_thms thyname int_thms thmnames
-				 |> clear_used_names
-				 |> export_hol4_pending
-				 |> Theory.parent_path
-				 |> dump_import_thy thyname
-				 |> add_dump ";end_setup"
-			 end)
+fun end_import toks =
+    Scan.succeed
+	(fn thy =>
+	    let
+		val thyname = get_generating_thy thy
+		val segname = get_import_segment thy
+		val (int_thms,facts) = Replay.setup_int_thms thyname thy
+		val thmnames = filter (not o should_ignore thyname thy) facts
+	    in
+		thy |> clear_import_thy
+		    |> set_segment thyname segname
+		    |> set_used_names facts
+		    |> Replay.import_thms thyname int_thms thmnames
+		    |> clear_used_names
+		    |> export_hol4_pending
+		    |> Theory.parent_path
+		    |> dump_import_thy thyname
+		    |> add_dump ";end_setup"
+	    end) toks
 
 val ignore_thms = Scan.repeat1 P.name
 			       >> (fn ignored =>
@@ -158,18 +159,20 @@
 			     | Generating _ => error "Currently generating a theory!"
 			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
 
-val end_setup = Scan.succeed (fn thy =>
-				 let
-				     val thyname = get_import_thy thy
-				     val segname = get_import_segment thy
-				 in
-				     thy |> set_segment thyname segname
-					 |> clear_import_thy
-					 |> Theory.parent_path
-				 end)
+fun end_setup toks =
+    Scan.succeed
+	(fn thy =>
+	    let
+		val thyname = get_import_thy thy
+		val segname = get_import_segment thy
+	    in
+		thy |> set_segment thyname segname
+		    |> clear_import_thy
+		    |> Theory.parent_path
+	    end) toks
 
 val set_dump  = P.string -- P.string   >> setup_dump
-val fl_dump   = Scan.succeed flush_dump
+fun fl_dump toks  = Scan.succeed flush_dump toks
 val append_dump = (P.verbatim || P.string) >> add_dump
 
 val parsers = 
diff -r 7ae3b247c6e9 -r c3019a66180f src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Apr 02 17:40:32 2004 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 04 15:34:14 2004 +0200
@@ -276,7 +276,7 @@
 
 fun get_segment thyname l = (Lib.assoc "s" l
 			     handle PK _ => thyname)
-val get_name    = Lib.assoc "n"
+val get_name : (string * string) list -> string = Lib.assoc "n"
 
 local
     open LazyScan
@@ -340,7 +340,11 @@
 val scan_start_of_tag = $$ #"<" |-- scan_id --
 			   repeat ($$ #" " |-- scan_attribute)
 
-val scan_end_of_tag = $$ #"/" |-- $$ #">" |-- succeed []
+(* The evaluation delay introduced through the 'toks' argument is needed
+for the sake of the SML/NJ (110.9.1) compiler.  Either that or an explicit
+type :-( *)
+fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
+
 val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
 
 fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
@@ -1633,7 +1637,7 @@
 	val cv = cterm_of sg v'
 	val th2 = norm_hyps th2
 	val cvty = ctyp_of_term cv
-	val _$c = concl_of th2
+	val c = HOLogic.dest_Trueprop (concl_of th2)
 	val cc = cterm_of sg c
 	val a = case concl_of th1 of
 		    _ $ (Const("Ex",_) $ a) => a
diff -r 7ae3b247c6e9 -r c3019a66180f src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Fri Apr 02 17:40:32 2004 +0200
+++ b/src/HOL/Import/shuffler.ML	Sun Apr 04 15:34:14 2004 +0200
@@ -263,7 +263,8 @@
 		  (([],tfree_names),tvars)
 	val t' = subst_TVars type_inst t
     in
-	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))) type_inst)
+	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
+		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
     end
 
 fun inst_tfrees sg [] thm = thm