global goals/qeds: after_qed operates on Proof.context (potentially local_theory);

--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Aug 08 18:40:56 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Aug 09 00:12:33 2006 +0200
@@ -3,18 +3,18 @@
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions. 
+A package for general recursive function definitions.
 Isar commands.
 
 *)
 
-signature FUNDEF_PACKAGE = 
+signature FUNDEF_PACKAGE =
 sig
     val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
 
     val cong_add: attribute
     val cong_del: attribute
-							 
+
     val setup : theory -> theory
     val get_congs : theory -> thm list
 end
@@ -27,24 +27,24 @@
 
 
 fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
-    let 
+    let
       val psimpss = Library.unflat (map snd spec_part) psimps
-      val (names, attss) = split_list (map fst spec_part) 
+      val (names, attss) = split_list (map fst spec_part)
 
-      val thy = thy |> Theory.add_path f_name 
-                
+      val thy = thy |> Theory.add_path f_name
+
       val thy = thy |> Theory.add_path label
       val spsimpss = map (map standard) psimpss (* FIXME *)
       val add_list = (names ~~ spsimpss) ~~ attss
       val (_, thy) = PureThy.add_thmss add_list thy
       val thy = thy |> Theory.parent_path
-                
+
       val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
       val thy = thy |> Theory.parent_path
     in
       thy
     end
-    
+
 
 
 
@@ -52,24 +52,24 @@
 
 fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
     let
-	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
-	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
+        val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
+        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
         val Mutual {parts, ...} = mutual_info
 
-	val Prep {names = Names {acc_R=accR, ...}, ...} = data
-	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
-	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
+        val Prep {names = Names {acc_R=accR, ...}, ...} = data
+        val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
+        val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
 
         val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
 
         val casenames = flat (map (map (fst o fst)) spec)
 
-	val thy = thy |> Theory.add_path name
-	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
-	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
-	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
-	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
-	val thy = thy |> Theory.parent_path
+        val thy = thy |> Theory.add_path name
+        val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
+        val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
+        val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
+        val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
+        val thy = thy |> Theory.parent_path
     in
       add_fundef_data name (fundef_data, mutual_info, spec) thy
     end
@@ -78,10 +78,10 @@
     let
       fun prep_eqns neqs =
           neqs
-            |> map (apsnd (Sign.read_prop thy))    
+            |> map (apsnd (Sign.read_prop thy))
             |> map (apfst (apsnd (apfst (map (prep_att thy)))))
             |> FundefSplit.split_some_equations (ProofContext.init thy)
-      
+
       val spec = map prep_eqns eqns_attss
       val t_eqnss = map (flat o map snd) spec
 
@@ -90,92 +90,94 @@
       val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
       val Prep {goal, goalI, ...} = data
     in
-	thy |> ProofContext.init
-	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", [])
-	    [(("", []), [(goal, [])])]
-            |> Proof.refine (Method.primitive_text (fn _ => goalI))
-            |> Seq.hd
+      thy |> ProofContext.init
+          |> Proof.theorem_i PureThy.internalK NONE
+              (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", [])
+              [(("", []), [(goal, [])])]
+          |> Proof.refine (Method.primitive_text (fn _ => goalI))
+          |> Seq.hd
     end
 
 
 fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
     let
-	val totality = hd (hd thmss)
+        val totality = hd (hd thmss)
 
-	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
-	  = the (get_fundef_data name thy)
+        val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
+          = the (get_fundef_data name thy)
 
-	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
 
-	val tsimps = map (map remove_domain_condition) psimps
-	val tinduct = map remove_domain_condition simple_pinducts
+        val tsimps = map (map remove_domain_condition) psimps
+        val tinduct = map remove_domain_condition simple_pinducts
 
         val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
         val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
 
         val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
 
-	val thy = Theory.add_path name thy
-		  
-	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
-	val thy = Theory.parent_path thy
+        val thy = Theory.add_path name thy
+
+        val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy
+        val thy = Theory.parent_path thy
     in
-	thy
+        thy
     end
 
 (*
 fun mk_partial_rules name D_name D domT idomT thmss thy =
     let
-	val [subs, dcl] = (hd thmss)
+        val [subs, dcl] = (hd thmss)
 
-	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
-	  = the (Symtab.lookup (FundefData.get thy) name)
+        val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
+          = the (Symtab.lookup (FundefData.get thy) name)
 
-	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
-						    [SOME (cterm_of thy D)]
-						    subsetD)
+        val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
+                                                    [SOME (cterm_of thy D)]
+                                                    subsetD)
 
-	val D_simps = map (curry op RS D_implies_dom) f_simps
+        val D_simps = map (curry op RS D_implies_dom) f_simps
 
-	val D_induct = subset_induct
-			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
-			   |> curry op COMP subs
-			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
-						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
+        val D_induct = subset_induct
+                           |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
+                           |> curry op COMP subs
+                           |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
+                                                 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
 
-	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
-	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
+        val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
+        val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
     in
-	thy3
+        thy3
     end
 *)
- 
+
 
-fun fundef_setup_termination_proof name NONE thy = 
+fun fundef_setup_termination_proof name NONE thy =
     let
-	val name = if name = "" then get_last_fundef thy else name
-	val data = the (get_fundef_data name thy)
+        val name = if name = "" then get_last_fundef thy else name
+        val data = the (get_fundef_data name thy)
                    handle Option.Option => raise ERROR ("No such function definition: " ^ name)
 
-	val (res as FundefMResult {termination, ...}, mutual, _) = data
-	val goal = FundefTermination.mk_total_termination_goal data
+        val (res as FundefMResult {termination, ...}, mutual, _) = data
+        val goal = FundefTermination.mk_total_termination_goal data
     in
-	thy |> ProofContext.init
-	    |> ProofContext.note_thmss_i [(("termination", 
-					    [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
-	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
-	    [(("", []), [(goal, [])])]
-    end	
+        thy |> ProofContext.init
+            |> ProofContext.note_thmss_i [(("termination",
+                                            [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
+            |> Proof.theorem_i PureThy.internalK NONE
+              (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", [])
+              [(("", []), [(goal, [])])]
+    end
   | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
     let
-	val name = if name = "" then get_last_fundef thy else name
-	val data = the (get_fundef_data name thy)
-	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
+        val name = if name = "" then get_last_fundef thy else name
+        val data = the (get_fundef_data name thy)
+        val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
     in
-	thy |> ProofContext.init
-	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
-	    [(("", []), [(subs, []), (dcl, [])])]
-    end	
+        thy |> ProofContext.init
+            |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
+            [(("", []), [(subs, []), (dcl, [])])]
+    end
 
 
 val add_fundef = gen_add_fundef Attrib.attribute
@@ -190,9 +192,9 @@
 
 (* setup *)
 
-val setup = FundefData.init #> FundefCongs.init 
-	#>  Attrib.add_attributes
-		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
+val setup = FundefData.init #> FundefCongs.init
+        #>  Attrib.add_attributes
+                [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
 
 
 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
@@ -207,7 +209,7 @@
 val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
 
 
-val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) 
+val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME))
                                                >> (fn x => (map_filter I x, exists is_none x)))
                               --| P.$$$ "]";
 
@@ -222,7 +224,7 @@
 
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --    
+  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --
   P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
                                     Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
 
@@ -230,7 +232,7 @@
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
        >> (fn (name,dom) =>
-	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
+              Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
 
 val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
 

--- a/src/Pure/Isar/isar_thy.ML	Tue Aug 08 18:40:56 2006 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Aug 09 00:12:33 2006 +0200
@@ -80,12 +80,14 @@
 fun apply_theorems args = apfst (maps snd) o theorems "" [(("", []), args)];
 fun apply_theorems_i args = apfst (maps snd) o theorems_i "" [(("", []), args)];
 
+(* FIXME local_theory *)
 fun smart_theorems kind NONE args thy = thy
       |> theorems kind args
       |> tap (present_theorems kind)
       |> (fn (_, thy) => `ProofContext.init thy)
   | smart_theorems kind (SOME loc) args thy = thy
       |> Locale.note_thmss kind loc args
+      ||> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt'))
       |> tap (fn ((_, res), (_, thy')) => present_theorems kind (res, thy'))
       |> #2;
 
@@ -131,7 +133,8 @@
 (* global endings *)
 
 fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state =>
-  if can (Proof.assert_bottom true) state then ending int state
+  if can (Proof.assert_bottom true) state then
+    ending int state |> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt'))
   else raise Toplevel.UNDEF);
 
 fun global_qed m = global_ending (K (Proof.global_qed (m, true)));

--- a/src/Pure/Isar/proof.ML	Tue Aug 08 18:40:56 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Aug 09 00:12:33 2006 +0200
@@ -94,19 +94,19 @@
   val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
     (theory -> 'a -> attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
-    string -> Method.text option -> (thm list list -> theory -> theory) ->
+    string -> Method.text option -> (thm list list -> context -> context) ->
     string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
-  val global_qed: Method.text option * bool -> state -> context * theory
+  val global_qed: Method.text option * bool -> state -> context
   val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
   val local_default_proof: state -> state Seq.seq
   val local_immediate_proof: state -> state Seq.seq
   val local_done_proof: state -> state Seq.seq
   val local_skip_proof: bool -> state -> state Seq.seq
-  val global_terminal_proof: Method.text * Method.text option -> state -> context * theory
-  val global_default_proof: state -> context * theory
-  val global_immediate_proof: state -> context * theory
-  val global_done_proof: state -> context * theory
-  val global_skip_proof: bool -> state -> context * theory
+  val global_terminal_proof: Method.text * Method.text option -> state -> context
+  val global_default_proof: state -> context
+  val global_immediate_proof: state -> context
+  val global_done_proof: state -> context
+  val global_skip_proof: bool -> state -> context
   val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
@@ -115,10 +115,10 @@
     ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
-  val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
+  val theorem: string -> Method.text option -> (thm list list -> context -> context) ->
     string option -> string * Attrib.src list ->
     ((string * Attrib.src list) * (string * string list) list) list -> context -> state
-  val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
+  val theorem_i: string -> Method.text option -> (thm list list -> context -> context) ->
     string option -> string * attribute list ->
     ((string * attribute list) * (term * term list) list) list -> context -> state
 end;
@@ -152,7 +152,7 @@
     before_qed: Method.text option,
     after_qed:
       (thm list list -> state -> state Seq.seq) *
-      (thm list list -> theory -> theory)};
+      (thm list list -> context -> context)};
 
 fun make_goal (statement, using, goal, before_qed, after_qed) =
   Goal {statement = statement, using = using, goal = goal,
@@ -386,10 +386,6 @@
 fun goal_cases st =
   RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
-fun check_theory thy state =
-  if subthy (thy, theory_of state) then state
-  else error ("Bad theory of method result: " ^ Context.str_of_thy thy);
-
 fun apply_method current_context meth_fun state =
   let
     val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
@@ -397,7 +393,6 @@
   in
     Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
       state
-      |> check_theory (Thm.theory_of_thm goal')
       |> map_goal
           (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
            ProofContext.add_cases true meth_cases)
@@ -881,10 +876,11 @@
       #> Sign.restore_naming thy;
 
     fun after_qed' results =
-      (case target of NONE => I
-      | SOME prfx => store_results (NameSpace.base prfx)
-          (map (ProofContext.export_standard ctxt thy_ctxt
-            #> map Drule.strip_shyps_warning) results))
+      ProofContext.theory
+        (case target of NONE => I
+        | SOME prfx => store_results (NameSpace.base prfx)
+            (map (ProofContext.export_standard ctxt thy_ctxt
+              #> map Drule.strip_shyps_warning) results))
       #> after_qed results;
   in
     init ctxt
@@ -900,8 +896,7 @@
 fun global_qeds txt =
   end_proof true txt
   #> Seq.map (generic_qed #> (fn (((_, after_qed), results), state) =>
-    after_qed results (theory_of state)
-    |> (fn thy => (ProofContext.transfer thy (context_of state), thy))))
+    after_qed results (context_of state)))
   |> Seq.DETERM;   (*backtracking may destroy theory!*)
 
 fun global_qed txt =

--- a/src/Pure/Isar/toplevel.ML	Tue Aug 08 18:40:56 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 09 00:12:33 2006 +0200
@@ -546,7 +546,8 @@
         warning "Cannot skip proof of schematic goal statement"
       else ();
       if ! skip_proofs andalso not schematic then
-        SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
+        SkipProof ((History.init (undo_limit int) 0,
+          ProofContext.theory_of (Proof.global_skip_proof int prf)), thy)
       else Proof (ProofHistory.init (undo_limit int) prf, thy)
     end
   | _ => raise UNDEF));