tuned;
authorwenzelm
Tue Jun 13 23:41:39 2006 +0200 (2006-06-13)
changeset 1987611d447d5d68c
parent 19875 7405ce9d4f25
child 19877 705ba8232952
tuned;
TFL/post.ML
TFL/rules.ML
TFL/tfl.ML
src/FOLP/simp.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/specification_package.ML
src/Pure/unify.ML
     1.1 --- a/TFL/post.ML	Tue Jun 13 23:41:37 2006 +0200
     1.2 +++ b/TFL/post.ML	Tue Jun 13 23:41:39 2006 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4    | tracing false msg = writeln msg;
     1.5  
     1.6  fun simplify_defn strict thy cs ss congs wfs id pats def0 =
     1.7 -   let val def = freezeT def0 RS meta_eq_to_obj_eq
     1.8 +   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
     1.9         val {theory,rules,rows,TCs,full_pats_TCs} =
    1.10             Prim.post_definition congs (thy, (def,pats))
    1.11         val {lhs=f,rhs} = S.dest_eq (concl def)
     2.1 --- a/TFL/rules.ML	Tue Jun 13 23:41:37 2006 +0200
     2.2 +++ b/TFL/rules.ML	Tue Jun 13 23:41:39 2006 +0200
     2.3 @@ -266,7 +266,7 @@
     2.4           | DL th (th1::rst) =
     2.5              let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
     2.6               in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
     2.7 -   in DL (freezeT disjth) (organize eq tml thl)
     2.8 +   in DL (Thm.freezeT disjth) (organize eq tml thl)
     2.9     end;
    2.10  
    2.11  
     3.1 --- a/TFL/tfl.ML	Tue Jun 13 23:41:37 2006 +0200
     3.2 +++ b/TFL/tfl.ML	Tue Jun 13 23:41:39 2006 +0200
     3.3 @@ -555,7 +555,7 @@
     3.4         thy
     3.5         |> PureThy.add_defs_i false
     3.6              [Thm.no_attributes (fid ^ "_def", defn)]
     3.7 -     val def = freezeT def0;
     3.8 +     val def = Thm.freezeT def0;
     3.9       val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
    3.10                             else ()
    3.11       (* val fconst = #lhs(S.dest_eq(concl def))  *)
     4.1 --- a/src/FOLP/simp.ML	Tue Jun 13 23:41:37 2006 +0200
     4.2 +++ b/src/FOLP/simp.ML	Tue Jun 13 23:41:39 2006 +0200
     4.3 @@ -222,7 +222,7 @@
     4.4  
     4.5  fun normed_rews congs =
     4.6    let val add_norms = add_norm_tags congs;
     4.7 -  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
     4.8 +  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
     4.9    end;
    4.10  
    4.11  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 13 23:41:37 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 13 23:41:39 2006 +0200
     5.3 @@ -51,7 +51,7 @@
     5.4  fun fundef_afterqed congs curry_info name data names atts thmss thy =
     5.5      let
     5.6  	val (complete_thm :: compat_thms) = map hd thmss
     5.7 -	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
     5.8 +	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms)
     5.9  	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
    5.10          val Mutual {parts, ...} = curry_info
    5.11  
     6.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 13 23:41:37 2006 +0200
     6.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 13 23:41:39 2006 +0200
     6.3 @@ -91,7 +91,7 @@
     6.4  	val localize = instantiate ([], cvqs ~~ cqs) 
     6.5  					   #> fold implies_elim_swp ags
     6.6  
     6.7 -	val GI = freezeT GI
     6.8 +	val GI = Thm.freezeT GI
     6.9  	val lGI = localize GI
    6.10  
    6.11  	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
    6.12 @@ -100,7 +100,7 @@
    6.13  	    let
    6.14  		fun mk_var0 (v,T) = Var ((v,0),T)
    6.15  
    6.16 -		val RI = freezeT RI
    6.17 +		val RI = Thm.freezeT RI
    6.18  		val lRI = localize RI
    6.19  		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
    6.20  		val plRI = prop_of lRI
    6.21 @@ -295,4 +295,4 @@
    6.22  
    6.23  
    6.24  
    6.25 -end
    6.26 \ No newline at end of file
    6.27 +end
     7.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 13 23:41:37 2006 +0200
     7.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Jun 13 23:41:39 2006 +0200
     7.3 @@ -439,7 +439,7 @@
     7.4  	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
     7.5      in
     7.6  	R_elim
     7.7 -	    |> freezeT
     7.8 +	    |> Thm.freezeT
     7.9  	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
    7.10  	    |> curry op COMP (assume z_ltR_x)
    7.11  	    |> fold_rev (curry op COMP) cases
    7.12 @@ -473,9 +473,9 @@
    7.13  	val compat_thms = map Drule.close_derivation compat_thms
    7.14  (*	val _ = Output.debug "  done"*)
    7.15  
    7.16 -	val complete_thm_fr = freezeT complete_thm
    7.17 -	val compat_thms_fr = map freezeT compat_thms
    7.18 -	val f_def_fr = freezeT f_def
    7.19 +	val complete_thm_fr = Thm.freezeT complete_thm
    7.20 +	val compat_thms_fr = map Thm.freezeT compat_thms
    7.21 +	val f_def_fr = Thm.freezeT f_def
    7.22  
    7.23  	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
    7.24  						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
    7.25 @@ -505,8 +505,8 @@
    7.26  	val var_order = get_var_order thy clauses
    7.27  	val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
    7.28  
    7.29 -	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> freezeT
    7.30 -	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> freezeT
    7.31 +	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> Thm.freezeT
    7.32 +	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> Thm.freezeT
    7.33  
    7.34  	val _ = Output.debug "Proving cases for unique existence..."
    7.35  	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
     8.1 --- a/src/HOL/Tools/function_package/mutual.ML	Tue Jun 13 23:41:37 2006 +0200
     8.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Jun 13 23:41:39 2006 +0200
     8.3 @@ -156,7 +156,7 @@
     8.4  
     8.5  	val x = Free ("x", RST)
     8.6  
     8.7 -	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (freezeT f_def) (* FIXME: freezeT *)
     8.8 +	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (Thm.freezeT f_def) (* FIXME: freezeT *)
     8.9      in
    8.10  	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
    8.11  		  |> (fn it => combination it (plain_eq RS eq_reflection))
     9.1 --- a/src/HOL/Tools/specification_package.ML	Tue Jun 13 23:41:37 2006 +0200
     9.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Jun 13 23:41:39 2006 +0200
     9.3 @@ -83,7 +83,7 @@
     9.4  end
     9.5  
     9.6  fun add_specification axiomatic cos arg =
     9.7 -    arg |> apsnd freezeT
     9.8 +    arg |> apsnd Thm.freezeT
     9.9          |> proc_exprop axiomatic cos
    9.10          |> apsnd standard
    9.11  
    9.12 @@ -223,7 +223,7 @@
    9.13                          then writeln "specification"
    9.14                          else ()
    9.15              in
    9.16 -                arg |> apsnd freezeT
    9.17 +                arg |> apsnd Thm.freezeT
    9.18                      |> process_all (zip3 alt_names rew_imps frees)
    9.19              end
    9.20              fun post_proc (context, th) =
    10.1 --- a/src/Pure/unify.ML	Tue Jun 13 23:41:37 2006 +0200
    10.2 +++ b/src/Pure/unify.ML	Tue Jun 13 23:41:39 2006 +0200
    10.3 @@ -31,8 +31,7 @@
    10.4  val trace_bound = ref 25  (*tracing starts above this depth, 0 for full*)
    10.5  and search_bound = ref 30 (*unification quits above this depth*)
    10.6  and trace_simp = ref false  (*print dpairs before calling SIMPL*)
    10.7 -and trace_types = ref false (*announce potential incompleteness
    10.8 -          of type unification*)
    10.9 +and trace_types = ref false (*announce potential incompleteness of type unification*)
   10.10  
   10.11  type binderlist = (string*typ) list;
   10.12  
   10.13 @@ -650,7 +649,7 @@
   10.14            in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
   10.15  
   10.16          fun result env =
   10.17 -          if Envir.above env maxidx then
   10.18 +          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
   10.19              SOME (Envir.Envir {maxidx = maxidx,
   10.20                iTs = Vartab.make (map (norm_tvar env) pat_tvars),
   10.21                asol = Vartab.make (map (norm_var env) pat_vars)})
   10.22 @@ -658,7 +657,8 @@
   10.23  
   10.24          val empty = Envir.empty maxidx';
   10.25        in
   10.26 -        Seq.append (pattern_matchers thy pairs empty)
   10.27 +        Seq.append
   10.28 +          (pattern_matchers thy pairs empty)
   10.29            (Seq.map_filter result (smash_unifiers thy pairs' empty))
   10.30        end;
   10.31