consts: ProofContext.set_stmt true -- avoids naming of local thms;
authorwenzelm
Wed, 22 Nov 2006 17:38:36 +0100
changeset 21467 4b0d5e8796cc
parent 21466 6ffb8f455b84
child 21468 c7892915ed10
consts: ProofContext.set_stmt true -- avoids naming of local thms;
src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Nov 22 15:58:59 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Nov 22 17:38:36 2006 +0100
@@ -78,7 +78,9 @@
   in
     lthy'
     |> K (loc <> "") ? (snd o LocalTheory.abbrevs Syntax.default_mode abbrs)
+    |> ProofContext.set_stmt true
     |> LocalDefs.add_defs defns |>> map (apsnd snd)
+    ||> ProofContext.restore_stmt lthy'
   end;