src/Pure/Isar/local_defs.ML
changeset 40242 bb433b0668b8
parent 39133 70d3915c92f0
child 41228 e1fce873b814
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Oct 28 23:19:52 2010 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Oct 28 23:54:39 2010 +0200
     1.3 @@ -44,8 +44,9 @@
     1.4  
     1.5  fun cert_def ctxt eq =
     1.6    let
     1.7 -    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
     1.8 -      quote (Syntax.string_of_term ctxt eq));
     1.9 +    fun err msg =
    1.10 +      cat_error msg ("The error(s) above occurred in definition:\n" ^
    1.11 +        quote (Syntax.string_of_term ctxt eq));
    1.12      val ((lhs, _), eq') = eq
    1.13        |> Sign.no_vars ctxt
    1.14        |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
    1.15 @@ -245,7 +246,7 @@
    1.16            (CONVERSION (meta_rewrite_conv ctxt') THEN'
    1.17              MetaSimplifier.rewrite_goal_tac [def] THEN'
    1.18              resolve_tac [Drule.reflexive_thm])))
    1.19 -        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
    1.20 +        handle ERROR msg => cat_error msg "Failed to prove definitional specification"
    1.21        end;
    1.22    in (((c, T), rhs), prove) end;
    1.23