src/Pure/Isar/expression.ML
changeset 43543 eb8b4851b039
parent 42494 eef1a23c9077
child 45289 25e9e7f527b4
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Jun 23 23:12:00 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Jun 25 12:19:54 2011 +0200
     1.3 @@ -797,6 +797,14 @@
     1.4  
     1.5  (*** Interpretation ***)
     1.6  
     1.7 +fun read_with_extended_syntax parse_prop deps ctxt props =
     1.8 +  let
     1.9 +    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    1.10 +  in
    1.11 +    map (parse_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
    1.12 +      |> Variable.export_terms deps_ctxt ctxt
    1.13 +  end;
    1.14 +
    1.15  (** Interpretation in theories and proof contexts **)
    1.16  
    1.17  local
    1.18 @@ -825,8 +833,8 @@
    1.19    let
    1.20      val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
    1.21        |> prep_expr expression;
    1.22 +    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.23  
    1.24 -    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.25      val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.26      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.27      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.28 @@ -845,8 +853,8 @@
    1.29      val theory = Proof_Context.theory_of ctxt;
    1.30  
    1.31      val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
    1.32 +    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.33  
    1.34 -    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.35      val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.36      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.37      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.38 @@ -904,8 +912,8 @@
    1.39      val target = intern thy raw_target;
    1.40      val target_ctxt = Named_Target.init before_exit target thy;
    1.41      val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.42 +    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.43  
    1.44 -    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.45      val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
    1.46      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.47      val export' = Variable.export_morphism goal_ctxt expr_ctxt;