# HG changeset patch
# User haftmann
# Date 1388007328 -3600
# Node ID 82bfac35f16fbb829940a711e7d541a01eb21546
# Parent  a064732223ad8d0db4f1c48f1d6b942c9dcfc00f
ephemeral interpretation also formally works on theory level

diff -r a064732223ad -r 82bfac35f16f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Dec 25 17:39:07 2013 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 25 22:35:28 2013 +0100
@@ -869,9 +869,6 @@
 
 (* various flavours of interpretation *)
 
-fun assert_not_theory lthy = if Named_Target.is_theory lthy
-  then error "Not possible on level of global theory" else ();
-
 fun gen_interpret prep_expr prep_prop prep_attr expression raw_eqns int state =
   let
     val _ = Proof.assert_forward_or_chain state;
@@ -897,7 +894,8 @@
 
 fun gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns lthy =
   let
-    val _ = assert_not_theory lthy;
+    val _ = if Named_Target.is_theory lthy
+      then error "Not possible on level of global theory" else ();
     val locale = Named_Target.the_name lthy;
   in
     lthy
@@ -931,13 +929,9 @@
   end;
 
 fun ephemeral_interpretation expression raw_eqns lthy =
-  let
-    val _ = assert_not_theory lthy;
-  in
-    lthy
-    |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
-        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
-  end;
+  lthy
+  |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
+      Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
 
 fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
 fun interpret_cmd x =