src/Pure/Isar/expression.ML
changeset 55997 9dc5ce83202c
parent 55639 e4e8cbd9d780
child 56057 ad6bd8030d88
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 08 13:49:01 2014 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 08 21:08:10 2014 +0100
     1.3 @@ -851,8 +851,7 @@
     1.4    let
     1.5      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
     1.6      val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
     1.7 -    val attrss =
     1.8 -      map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
     1.9 +    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
    1.10      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.11      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.12    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.13 @@ -861,7 +860,7 @@
    1.14    prep_interpretation cert_goal_expression (K I) (K I);
    1.15  
    1.16  val read_interpretation =
    1.17 -  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src;
    1.18 +  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.check_src;
    1.19  
    1.20  
    1.21  (* generic interpretation machinery *)