# HG changeset patch # User wenzelm # Date 1208012438 -7200 # Node ID dac6d56b7c8dde229d1594659a99c1344a68fbe3 # Parent c6231d64d264ff6c7a790d5f12e6bf0b71f88234 rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression); diff -r c6231d64d264 -r dac6d56b7c8d src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sat Apr 12 17:00:35 2008 +0200 +++ b/src/HOL/Tools/res_axioms.ML Sat Apr 12 17:00:38 2008 +0200 @@ -272,7 +272,8 @@ let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) val (ch, frees) = c_variant_abs_multi (rhs, []) val (chilbert,cabs) = Thm.dest_comb ch - val {thy,t, ...} = rep_cterm chilbert + val thy = Thm.theory_of_cterm chilbert + val t = Thm.term_of chilbert val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T | _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) val cex = Thm.cterm_of thy (HOLogic.exists_const T) @@ -383,7 +384,7 @@ val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 - |> Meson.finish_cnf |> map Goal.close_result + |> Meson.finish_cnf |> map Thm.close_derivation in (cnfs', thy') end handle Clausify_failure thy_e => ([],thy_e) ) @@ -430,7 +431,7 @@ in case Thmtab.lookup (ThmCache.get thy) th of NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); - map Goal.close_result (skolem_thm (fake_name th, th))) + map Thm.close_derivation (skolem_thm (fake_name th, th))) | SOME cls => cls end; diff -r c6231d64d264 -r dac6d56b7c8d src/Pure/drule.ML --- a/src/Pure/drule.ML Sat Apr 12 17:00:35 2008 +0200 +++ b/src/Pure/drule.ML Sat Apr 12 17:00:38 2008 +0200 @@ -87,7 +87,6 @@ val beta_conv: cterm -> cterm -> cterm val add_used: thm -> string list -> string list val flexflex_unique: thm -> thm - val close_derivation: thm -> thm val store_thm: bstring -> thm -> thm val store_standard_thm: bstring -> thm -> thm val store_thm_open: bstring -> thm -> thm @@ -152,13 +151,8 @@ (*The premises of a theorem, as a cterm list*) val cprems_of = strip_imp_prems o cprop_of; -fun cterm_fun f ct = - let val {t, thy, ...} = Thm.rep_cterm ct - in Thm.cterm_of thy (f t) end; - -fun ctyp_fun f cT = - let val {T, thy, ...} = Thm.rep_ctyp cT - in Thm.ctyp_of thy (f T) end; +fun cterm_fun f ct = Thm.cterm_of (Thm.theory_of_cterm ct) (f (Thm.term_of ct)); +fun ctyp_fun f cT = Thm.ctyp_of (Thm.theory_of_ctyp cT) (f (Thm.typ_of cT)); fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t; @@ -284,7 +278,8 @@ (*Generalization over all suitable Free variables*) fun forall_intr_frees th = let - val {prop, hyps, tpairs, thy,...} = rep_thm th; + val thy = Thm.theory_of_thm th; + val {prop, hyps, tpairs, ...} = rep_thm th; val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) []; val frees = Term.fold_aterms (fn Free v => if member (op =) fixed v then I else insert (op =) v | _ => I) prop []; @@ -305,7 +300,8 @@ (*generalize outermost parameters*) fun gen_all th = let - val {thy, prop, maxidx, ...} = Thm.rep_thm th; + val thy = Thm.theory_of_thm th; + val {prop, maxidx, ...} = Thm.rep_thm th; val cert = Thm.cterm_of thy; fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T))); in fold elim (outer_params prop) th end; @@ -369,10 +365,6 @@ | [] => raise THM("flexflex_unique: impossible constraints", 0, [th]) | _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]); -fun close_derivation thm = - if Thm.get_name thm = "" then Thm.put_name "" thm - else thm; - (* legacy standard operations *) @@ -384,13 +376,12 @@ forall_elim_vars (maxidx + 1) #> Thm.strip_shyps #> zero_var_indexes - #> Thm.varifyT - #> Thm.compress); + #> Thm.varifyT); val standard = flexflex_unique #> standard' - #> close_derivation; + #> Thm.close_derivation; (*Convert all Vars in a theorem to Frees. Also return a function for @@ -399,7 +390,8 @@ fun freeze_thaw_robust th = let val fth = Thm.freezeT th - val {prop, tpairs, thy, ...} = rep_thm fth + val thy = Thm.theory_of_thm fth + val {prop, tpairs, ...} = rep_thm fth in case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*) @@ -421,7 +413,8 @@ clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*) fun freeze_thaw th = let val fth = Thm.freezeT th - val {prop, tpairs, thy, ...} = rep_thm fth + val thy = Thm.theory_of_thm fth + val {prop, tpairs, ...} = rep_thm fth in case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of [] => (fth, fn x => x) @@ -829,8 +822,11 @@ Instantiates distinct Vars by terms, inferring type instantiations. *) local fun add_types ((ct,cu), (thy,tye,maxidx)) = - let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct - and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; + let + val thyt = Thm.theory_of_cterm ct; + val thyu = Thm.theory_of_cterm cu; + val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; + val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu; val maxi = Int.max(maxidx, Int.max(maxt, maxu)); val thy' = Theory.merge(thy, Theory.merge(thyt, thyu)) val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) @@ -887,9 +883,10 @@ fun mk_term ct = let - val {thy, T, ...} = Thm.rep_cterm ct; + val thy = Thm.theory_of_cterm ct; val cert = Thm.cterm_of thy; val certT = Thm.ctyp_of thy; + val T = Thm.typ_of (Thm.ctyp_of_term ct); val a = certT (TVar (("'a", 0), [])); val x = cert (Var (("x", 0), T)); in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end; @@ -951,19 +948,20 @@ fun rename_bvars [] thm = thm | rename_bvars vs thm = - let - val {thy, prop, ...} = rep_thm thm; - fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t) - | ren (t $ u) = ren t $ ren u - | ren t = t; - in equal_elim (reflexive (cterm_of thy (ren prop))) thm end; + let + val cert = Thm.cterm_of (Thm.theory_of_thm thm); + fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t) + | ren (t $ u) = ren t $ ren u + | ren t = t; + in equal_elim (reflexive (cert (ren (Thm.prop_of thm)))) thm end; (* renaming in left-to-right order *) fun rename_bvars' xs thm = let - val {thy, prop, ...} = rep_thm thm; + val cert = Thm.cterm_of (Thm.theory_of_thm thm); + val prop = Thm.prop_of thm; fun rename [] t = ([], t) | rename (x' :: xs) (Abs (x, T, t)) = let val (xs', t') = rename xs t @@ -975,7 +973,7 @@ in (xs'', t' $ u') end | rename xs t = (xs, t); in case rename xs prop of - ([], prop') => equal_elim (reflexive (cterm_of thy prop')) thm + ([], prop') => equal_elim (reflexive (cert prop')) thm | _ => error "More names than abstractions in theorem" end;