src/HOL/Import/proof_kernel.ML
changeset 27187 17b63e145986
parent 26939 1035c89b4c02
child 27353 71c4dd53d4cb
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jun 12 22:41:03 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jun 12 23:12:54 2008 +0200
     1.3 @@ -236,7 +236,7 @@
     1.4                  else F (n+1)
     1.5              end
     1.6              handle ERROR mesg => F (n+1)
     1.7 -                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
     1.8 +                 | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
     1.9      in
    1.10        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    1.11      end