1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Sep 02 23:37:14 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Sep 02 23:45:37 2010 +0200
     1.3 @@ -741,14 +741,14 @@
     1.4    let
     1.5      val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
     1.6      val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
     1.7 -      handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
     1.8 +      handle ERROR msg => cat_error msg "Failed to parse sort";
     1.9    in Type.minimize_sort (tsig_of ctxt) S end;
    1.10  
    1.11  fun parse_typ ctxt text =
    1.12    let
    1.13      val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    1.14      val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
    1.15 -      handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
    1.16 +      handle ERROR msg => cat_error msg "Failed to parse type";
    1.17    in T end;
    1.18  
    1.19  fun parse_term T ctxt text =
    1.20 @@ -756,7 +756,8 @@
    1.21      val {get_sort, map_const, map_free} = term_context ctxt;
    1.22  
    1.23      val (T', _) = Type_Infer.paramify_dummies T 0;
    1.24 -    val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    1.25 +    val (markup, kind) =
    1.26 +      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    1.27      val (syms, pos) = Syntax.parse_token ctxt markup text;
    1.28  
    1.29      fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
    1.30 @@ -764,7 +765,7 @@
    1.31      val t =
    1.32        Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
    1.33          ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
    1.34 -      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
    1.35 +      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
    1.36    in t end;
    1.37  
    1.38