author | wenzelm |
Mon, 20 Mar 2006 21:29:04 +0100 | |
changeset 19296 | ad96f1095dca |
parent 19295 | c5d236fe9668 |
child 19297 | 8f6e097d7b23 |
--- 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;