LocalTheory.exit_global;
authorwenzelm
Mon Sep 29 10:58:01 2008 +0200 (2008-09-29)
changeset 28394b9c8e3a12a98
parent 28393 30ba169e8c45
child 28395 984fcc8feb24
LocalTheory.exit_global;
src/HOL/Code_Eval.thy
src/HOL/Library/RType.thy
src/HOL/Statespace/state_space.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Typedef.thy
src/HOL/ex/Quickcheck.thy
src/HOLCF/Tools/pcpodef_package.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/HOL/Code_Eval.thy	Sun Sep 28 14:46:51 2008 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Mon Sep 29 10:58:01 2008 +0200
     1.3 @@ -70,8 +70,7 @@
     1.4        |-> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))
     1.5        |> snd
     1.6        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     1.7 -      |> LocalTheory.exit
     1.8 -      |> ProofContext.theory_of
     1.9 +      |> LocalTheory.exit_global
    1.10      end;
    1.11    fun interpretator (tyco, (raw_vs, _)) thy =
    1.12      let
     2.1 --- a/src/HOL/Library/RType.thy	Sun Sep 28 14:46:51 2008 +0200
     2.2 +++ b/src/HOL/Library/RType.thy	Mon Sep 29 10:58:01 2008 +0200
     2.3 @@ -70,8 +70,7 @@
     2.4      |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     2.5      |> snd
     2.6      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     2.7 -    |> LocalTheory.exit
     2.8 -    |> ProofContext.theory_of
     2.9 +    |> LocalTheory.exit_global
    2.10    end;
    2.11  
    2.12  fun perhaps_add_def tyco thy =
     3.1 --- a/src/HOL/Statespace/state_space.ML	Sun Sep 28 14:46:51 2008 +0200
     3.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Sep 29 10:58:01 2008 +0200
     3.3 @@ -352,8 +352,7 @@
     3.4    thy
     3.5    |> TheoryTarget.init name
     3.6    |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
     3.7 -  |> LocalTheory.exit
     3.8 -  |> ProofContext.theory_of;
     3.9 +  |> LocalTheory.exit_global;
    3.10  
    3.11  fun parent_components thy (Ts, pname, renaming) =
    3.12    let
     4.1 --- a/src/HOL/Tools/datatype_codegen.ML	Sun Sep 28 14:46:51 2008 +0200
     4.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Sep 29 10:58:01 2008 +0200
     4.3 @@ -471,8 +471,7 @@
     4.4      |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
     4.5      |> fold_map add_def dtcos
     4.6      |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
     4.7 -    #> LocalTheory.exit
     4.8 -    #> ProofContext.theory_of
     4.9 +    #> LocalTheory.exit_global
    4.10      #> fold Code.del_eqn thms
    4.11      #> fold add_eq_thms dtcos)
    4.12    end;
     5.1 --- a/src/HOL/Tools/function_package/size.ML	Sun Sep 28 14:46:51 2008 +0200
     5.2 +++ b/src/HOL/Tools/function_package/size.ML	Mon Sep 29 10:58:01 2008 +0200
     5.3 @@ -151,8 +151,7 @@
     5.4        ||>> fold_map define_overloaded
     5.5          (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
     5.6        ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     5.7 -      ||> LocalTheory.exit
     5.8 -      ||> ProofContext.theory_of;
     5.9 +      ||> LocalTheory.exit_global;
    5.10  
    5.11      val ctxt = ProofContext.init thy';
    5.12  
     6.1 --- a/src/HOL/Tools/primrec_package.ML	Sun Sep 28 14:46:51 2008 +0200
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Sep 29 10:58:01 2008 +0200
     6.3 @@ -279,14 +279,14 @@
     6.4      val lthy = TheoryTarget.init NONE thy;
     6.5      val (simps, lthy') = add_primrec fixes specs lthy;
     6.6      val simps' = ProofContext.export lthy' lthy simps;
     6.7 -  in (simps', ProofContext.theory_of (LocalTheory.exit lthy')) end;
     6.8 +  in (simps', LocalTheory.exit_global lthy') end;
     6.9  
    6.10  fun add_primrec_overloaded ops fixes specs thy =
    6.11    let
    6.12      val lthy = TheoryTarget.overloading ops thy;
    6.13      val (simps, lthy') = add_primrec fixes specs lthy;
    6.14      val simps' = ProofContext.export lthy' lthy simps;
    6.15 -  in (simps', ProofContext.theory_of (LocalTheory.exit lthy')) end;
    6.16 +  in (simps', LocalTheory.exit_global lthy') end;
    6.17  
    6.18  
    6.19  (* outer syntax *)
     7.1 --- a/src/HOL/Tools/typecopy_package.ML	Sun Sep 28 14:46:51 2008 +0200
     7.2 +++ b/src/HOL/Tools/typecopy_package.ML	Mon Sep 29 10:58:01 2008 +0200
     7.3 @@ -161,8 +161,7 @@
     7.4      |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
     7.5      |> add_def tyco
     7.6      |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
     7.7 -    #> LocalTheory.exit
     7.8 -    #> ProofContext.theory_of
     7.9 +    #> LocalTheory.exit_global
    7.10      #> Code.del_eqn thm
    7.11      #> add_eq_thms)
    7.12    end;
     8.1 --- a/src/HOL/Typedef.thy	Sun Sep 28 14:46:51 2008 +0200
     8.2 +++ b/src/HOL/Typedef.thy	Mon Sep 29 10:58:01 2008 +0200
     8.3 @@ -148,8 +148,7 @@
     8.4      |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     8.5      |> snd
     8.6      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     8.7 -    |> LocalTheory.exit
     8.8 -    |> ProofContext.theory_of
     8.9 +    |> LocalTheory.exit_global
    8.10    end
    8.11  in TypedefPackage.interpretation add_itself end
    8.12  *}
     9.1 --- a/src/HOL/ex/Quickcheck.thy	Sun Sep 28 14:46:51 2008 +0200
     9.2 +++ b/src/HOL/ex/Quickcheck.thy	Mon Sep 29 10:58:01 2008 +0200
     9.3 @@ -157,8 +157,7 @@
     9.4            |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     9.5            |> snd
     9.6            |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     9.7 -          |> LocalTheory.exit
     9.8 -          |> ProofContext.theory_of
     9.9 +          |> LocalTheory.exit_global
    9.10          end
    9.11      | random_inst tycos thy = raise REC
    9.12          ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
    10.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sun Sep 28 14:46:51 2008 +0200
    10.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Mon Sep 29 10:58:01 2008 +0200
    10.3 @@ -100,8 +100,7 @@
    10.4          val thy5 = lthy4
    10.5            |> Class.prove_instantiation_instance
    10.6                (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
    10.7 -          |> LocalTheory.exit
    10.8 -          |> ProofContext.theory_of;
    10.9 +          |> LocalTheory.exit_global;
   10.10        in ((type_definition, less_definition, set_def), thy5) end;
   10.11  
   10.12      fun make_cpo admissible (type_def, less_def, set_def) theory =
    11.1 --- a/src/Pure/Isar/toplevel.ML	Sun Sep 28 14:46:51 2008 +0200
    11.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Sep 29 10:58:01 2008 +0200
    11.3 @@ -109,7 +109,7 @@
    11.4  type generic_theory = Context.generic;    (*theory or local_theory*)
    11.5  
    11.6  val loc_init = TheoryTarget.context;
    11.7 -val loc_exit = ProofContext.theory_of o LocalTheory.exit;
    11.8 +val loc_exit = LocalTheory.exit_global;
    11.9  
   11.10  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   11.11    | loc_begin NONE (Context.Proof lthy) = lthy