src/Pure/Isar/expression.ML
changeset 54865 82bfac35f16f
parent 54742 7a86358a3c0b
child 54875 b370e1622e41
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 25 17:39:07 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 25 22:35:28 2013 +0100
     1.3 @@ -869,9 +869,6 @@
     1.4  
     1.5  (* various flavours of interpretation *)
     1.6  
     1.7 -fun assert_not_theory lthy = if Named_Target.is_theory lthy
     1.8 -  then error "Not possible on level of global theory" else ();
     1.9 -
    1.10  fun gen_interpret prep_expr prep_prop prep_attr expression raw_eqns int state =
    1.11    let
    1.12      val _ = Proof.assert_forward_or_chain state;
    1.13 @@ -897,7 +894,8 @@
    1.14  
    1.15  fun gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns lthy =
    1.16    let
    1.17 -    val _ = assert_not_theory lthy;
    1.18 +    val _ = if Named_Target.is_theory lthy
    1.19 +      then error "Not possible on level of global theory" else ();
    1.20      val locale = Named_Target.the_name lthy;
    1.21    in
    1.22      lthy
    1.23 @@ -931,13 +929,9 @@
    1.24    end;
    1.25  
    1.26  fun ephemeral_interpretation expression raw_eqns lthy =
    1.27 -  let
    1.28 -    val _ = assert_not_theory lthy;
    1.29 -  in
    1.30 -    lthy
    1.31 -    |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
    1.32 -        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
    1.33 -  end;
    1.34 +  lthy
    1.35 +  |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
    1.36 +      Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
    1.37  
    1.38  fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
    1.39  fun interpret_cmd x =