# HG changeset patch
# User wenzelm
# Date 1257455327 -3600
# Node ID 0fc03a81c27c8a0cf7bebd9f9160d443e42a3675
# Parent  fbd47f9b9b1213ef5f1f8b36346efe8ed135e174
adapted LocalTheory.declaration;

diff -r fbd47f9b9b12 -r 0fc03a81c27c src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -355,7 +355,7 @@
 fun add_declaration name decl thy =
   thy
   |> TheoryTarget.init name
-  |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
+  |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
   |> LocalTheory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
diff -r fbd47f9b9b12 -r 0fc03a81c27c src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -118,7 +118,7 @@
             else Specification.print_consts lthy (K false) (map fst fixes)
         in
           lthy
-          |> LocalTheory.declaration (add_function_data o morph_function_data cdata)
+          |> LocalTheory.declaration false (add_function_data o morph_function_data cdata)
         end
     in
       lthy
diff -r fbd47f9b9b12 -r 0fc03a81c27c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -792,7 +792,7 @@
        induct = induct};
 
     val ctxt3 = ctxt2
-      |> LocalTheory.declaration (fn phi =>
+      |> LocalTheory.declaration false (fn phi =>
         let val result' = morph_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
   in (result, ctxt3) end;
diff -r fbd47f9b9b12 -r 0fc03a81c27c src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -41,7 +41,7 @@
 val get = Item_Net.content o Rules.get o Context.Proof;
 val get_global = Item_Net.content o Rules.get o Context.Theory;
 
-fun add class (ts, ths) = LocalTheory.declaration
+fun add class (ts, ths) = LocalTheory.declaration true
   (fn phi =>
     let
       val ts' = map (Morphism.term phi) ts;
diff -r fbd47f9b9b12 -r 0fc03a81c27c src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Nov 05 22:06:46 2009 +0100
+++ b/src/Pure/simplifier.ML	Thu Nov 05 22:08:47 2009 +0100
@@ -192,7 +192,7 @@
        identifier = identifier}
       |> morph_simproc (LocalTheory.target_morphism lthy);
   in
-    lthy |> LocalTheory.declaration (fn phi =>
+    lthy |> LocalTheory.declaration false (fn phi =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;