--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Nov 30 14:17:25 2006 +0100
@@ -74,8 +74,8 @@
val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
val qualify = NameSpace.qualified defname
-
- val (((psimps', pinducts'), (_, [termination'])), lthy) =
+
+ val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
|> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
@@ -86,7 +86,7 @@
val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
pinducts=snd pinducts', termination=termination', f=f, R=R }
-
+
in
lthy (* FIXME proper handling of morphism *)
|> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
@@ -135,7 +135,7 @@
let
val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
- val totality = PROFILE "closing" Drule.close_derivation totality
+ val totality = PROFILE "closing" Goal.close_result totality
val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
@@ -145,7 +145,7 @@
(* FIXME: How to generate code from (possibly) local contexts*)
val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
-
+
val qualify = NameSpace.qualified defname;
in
lthy
@@ -164,8 +164,9 @@
val goal = FundefTermination.mk_total_termination_goal f R
in
lthy
- |> ProofContext.note_thmss_i "" [(("termination",
- [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
+ |> ProofContext.note_thmss_i ""
+ [(("termination", [ContextRules.intro_query NONE]),
+ [([Goal.norm_result termination], [])])] |> snd
|> set_termination_rule termination
|> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
end
@@ -184,23 +185,23 @@
(* Datatype hook to declare datatype congs as "fundef_congs" *)
-fun add_case_cong n thy =
- Context.theory_map (map_fundef_congs (Drule.add_rule
+fun add_case_cong n thy =
+ Context.theory_map (map_fundef_congs (Drule.add_rule
(DatatypePackage.get_datatype thy n |> the
|> #case_cong
- |> safe_mk_meta_eq)))
+ |> safe_mk_meta_eq)))
thy
val case_cong_hook = fold add_case_cong
-val setup_case_cong_hook =
+val setup_case_cong_hook =
DatatypeHooks.add case_cong_hook
#> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
(* setup *)
-val setup =
- FundefData.init
+val setup =
+ FundefData.init
#> FundefCongs.init
#> TerminationRule.init
#> Attrib.add_attributes
--- a/src/HOL/Tools/function_package/fundef_prep.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Thu Nov 30 14:17:25 2006 +0100
@@ -237,7 +237,7 @@
|> fold_rev (implies_intr o cprop_of) h_assums
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr cqs
- |> Drule.close_derivation
+ |> Goal.close_result
in
replace_lemma
end
@@ -367,7 +367,7 @@
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
val goal = complete COMP (graph_is_function COMP conjunctionI)
- |> Drule.close_derivation
+ |> Goal.close_result
val goalI = Goal.protect goal
|> fold_rev (implies_intr o cprop_of) compat
--- a/src/HOL/Tools/function_package/fundef_proof.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Thu Nov 30 14:17:25 2006 +0100
@@ -299,7 +299,7 @@
let
val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
- val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal
+ val provedgoal = PROFILE "Closing result" Goal.close_result provedgoal
val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
--- a/src/HOL/Tools/res_axioms.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Nov 30 14:17:25 2006 +0100
@@ -485,7 +485,7 @@
(case skolem thy (name, Thm.transfer thy th) of
NONE => ([th],thy)
| SOME (thy',cls) =>
- let val cls = map Drule.local_standard cls
+ let val cls = map Goal.close_result cls
in
if null cls then warning ("skolem_cache: empty clause set for " ^ name)
else ();
@@ -506,7 +506,7 @@
"" => skolem_thm th (*no name, so can't cache*)
| s => case Symtab.lookup (!clause_cache) s of
NONE =>
- let val cls = map Drule.local_standard (skolem_thm th)
+ let val cls = map Goal.close_result (skolem_thm th)
in Output.debug "inserted into cache";
change clause_cache (Symtab.update (s, (th, cls))); cls
end
--- a/src/Pure/Isar/locale.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/Pure/Isar/locale.ML Thu Nov 30 14:17:25 2006 +0100
@@ -1809,7 +1809,8 @@
val (ctxt, (_, facts)) = activate_facts true (K I)
(ProofContext.init pred_thy, axiomify predicate_axioms elemss');
val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
- val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
+ val export = Goal.close_result o Goal.norm_result o
+ singleton (ProofContext.export view_ctxt thy_ctxt);
val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
--- a/src/Pure/Isar/specification.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/Pure/Isar/specification.ML Thu Nov 30 14:17:25 2006 +0100
@@ -273,7 +273,9 @@
prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
fun after_qed' results goal_ctxt' =
- let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
+ let val results' =
+ burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
+ in
lthy
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>