--- 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)
--- 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;
--- 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)) *)
--- 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];
--- 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
--- 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
--- 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)
--- 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))
--- 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) =
--- 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;