# HG changeset patch
# User wenzelm
# Date 1150234899 -7200
# Node ID 11d447d5d68cae9d8139af559f01ef34e6b915eb
# Parent  7405ce9d4f25534a12d6106dec85da9bad7fb41b
tuned;

diff -r 7405ce9d4f25 -r 11d447d5d68c TFL/post.ML
--- a/TFL/post.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/TFL/post.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -170,7 +170,7 @@
   | tracing false msg = writeln msg;
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
-   let val def = freezeT def0 RS meta_eq_to_obj_eq
+   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
        val {theory,rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)
diff -r 7405ce9d4f25 -r 11d447d5d68c TFL/rules.ML
--- a/TFL/rules.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/TFL/rules.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -266,7 +266,7 @@
          | DL th (th1::rst) =
             let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
              in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
-   in DL (freezeT disjth) (organize eq tml thl)
+   in DL (Thm.freezeT disjth) (organize eq tml thl)
    end;
 
 
diff -r 7405ce9d4f25 -r 11d447d5d68c TFL/tfl.ML
--- a/TFL/tfl.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/TFL/tfl.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -555,7 +555,7 @@
        thy
        |> PureThy.add_defs_i false
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = freezeT def0;
+     val def = Thm.freezeT def0;
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
                            else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)
diff -r 7405ce9d4f25 -r 11d447d5d68c src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/FOLP/simp.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -222,7 +222,7 @@
 
 fun normed_rews congs =
   let val add_norms = add_norm_tags congs;
-  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
+  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
   end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
diff -r 7405ce9d4f25 -r 11d447d5d68c src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -51,7 +51,7 @@
 fun fundef_afterqed congs curry_info name data names atts thmss thy =
     let
 	val (complete_thm :: compat_thms) = map hd thmss
-	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
+	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms)
 	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
         val Mutual {parts, ...} = curry_info
 
diff -r 7405ce9d4f25 -r 11d447d5d68c src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -91,7 +91,7 @@
 	val localize = instantiate ([], cvqs ~~ cqs) 
 					   #> fold implies_elim_swp ags
 
-	val GI = freezeT GI
+	val GI = Thm.freezeT GI
 	val lGI = localize GI
 
 	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
@@ -100,7 +100,7 @@
 	    let
 		fun mk_var0 (v,T) = Var ((v,0),T)
 
-		val RI = freezeT RI
+		val RI = Thm.freezeT RI
 		val lRI = localize RI
 		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
 		val plRI = prop_of lRI
@@ -295,4 +295,4 @@
 
 
 
-end
\ No newline at end of file
+end
diff -r 7405ce9d4f25 -r 11d447d5d68c src/HOL/Tools/function_package/fundef_proof.ML
--- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -439,7 +439,7 @@
 	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
     in
 	R_elim
-	    |> freezeT
+	    |> Thm.freezeT
 	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
 	    |> curry op COMP (assume z_ltR_x)
 	    |> fold_rev (curry op COMP) cases
@@ -473,9 +473,9 @@
 	val compat_thms = map Drule.close_derivation compat_thms
 (*	val _ = Output.debug "  done"*)
 
-	val complete_thm_fr = freezeT complete_thm
-	val compat_thms_fr = map freezeT compat_thms
-	val f_def_fr = freezeT f_def
+	val complete_thm_fr = Thm.freezeT complete_thm
+	val compat_thms_fr = map Thm.freezeT compat_thms
+	val f_def_fr = Thm.freezeT f_def
 
 	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
 						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
@@ -505,8 +505,8 @@
 	val var_order = get_var_order thy clauses
 	val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
 
-	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> freezeT
-	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> freezeT
+	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> Thm.freezeT
+	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> Thm.freezeT
 
 	val _ = Output.debug "Proving cases for unique existence..."
 	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
diff -r 7405ce9d4f25 -r 11d447d5d68c src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -156,7 +156,7 @@
 
 	val x = Free ("x", RST)
 
-	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (freezeT f_def) (* FIXME: freezeT *)
+	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (Thm.freezeT f_def) (* FIXME: freezeT *)
     in
 	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
 		  |> (fn it => combination it (plain_eq RS eq_reflection))
diff -r 7405ce9d4f25 -r 11d447d5d68c src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -83,7 +83,7 @@
 end
 
 fun add_specification axiomatic cos arg =
-    arg |> apsnd freezeT
+    arg |> apsnd Thm.freezeT
         |> proc_exprop axiomatic cos
         |> apsnd standard
 
@@ -223,7 +223,7 @@
                         then writeln "specification"
                         else ()
             in
-                arg |> apsnd freezeT
+                arg |> apsnd Thm.freezeT
                     |> process_all (zip3 alt_names rew_imps frees)
             end
             fun post_proc (context, th) =
diff -r 7405ce9d4f25 -r 11d447d5d68c src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Jun 13 23:41:37 2006 +0200
+++ b/src/Pure/unify.ML	Tue Jun 13 23:41:39 2006 +0200
@@ -31,8 +31,7 @@
 val trace_bound = ref 25  (*tracing starts above this depth, 0 for full*)
 and search_bound = ref 30 (*unification quits above this depth*)
 and trace_simp = ref false  (*print dpairs before calling SIMPL*)
-and trace_types = ref false (*announce potential incompleteness
-          of type unification*)
+and trace_types = ref false (*announce potential incompleteness of type unification*)
 
 type binderlist = (string*typ) list;
 
@@ -650,7 +649,7 @@
           in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
 
         fun result env =
-          if Envir.above env maxidx then
+          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
             SOME (Envir.Envir {maxidx = maxidx,
               iTs = Vartab.make (map (norm_tvar env) pat_tvars),
               asol = Vartab.make (map (norm_var env) pat_vars)})
@@ -658,7 +657,8 @@
 
         val empty = Envir.empty maxidx';
       in
-        Seq.append (pattern_matchers thy pairs empty)
+        Seq.append
+          (pattern_matchers thy pairs empty)
           (Seq.map_filter result (smash_unifiers thy pairs' empty))
       end;