src/Pure/Isar/expression.ML

   in setup_proof after_qed propss eqns goal_ctxt end;
 
 
 (* 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;
     val ctxt = Proof.context_of state;
     fun lift_after_qed after_qed witss eqns = Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;

     |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
         Local_Theory.notes_kind Local_Theory.activate expression raw_eqns;
 
 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
     |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
         Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns

     |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
         Local_Theory.notes_kind subscribe expression raw_eqns
   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 =
   gen_interpret read_goal_expression Syntax.parse_prop Attrib.intern_src x;