# HG changeset patch
# User wenzelm
# Date 1142886544 -3600
# Node ID ad96f1095dca2af636fd599f209ebd69924a859b
# Parent  c5d236fe96684fb847a4b05e5bfdc30c1135e7c6
interpret: Proof.assert_forward_or_chain;

diff -r c5d236fe9668 -r ad96f1095dca src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Mar 20 17:38:22 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 20 21:29:04 2006 +0100
@@ -2190,6 +2190,7 @@
 
 fun interpret (prfx, atts) expr insts int state =
   let
+    val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
     val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
     val kind = goal_name (Proof.theory_of state) "interpret" NONE propss;