eliminated obsolete print_sign_exn_unit;
authorwenzelm
Wed Jan 12 15:09:26 2011 +0100 (2011-01-12)
changeset 41521c704c437ec74
parent 41520 3470b54e95d6
child 41522 42d13d00ccfb
eliminated obsolete print_sign_exn_unit;
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed Jan 12 15:08:21 2011 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed Jan 12 15:09:26 2011 +0100
     1.3 @@ -35,27 +35,6 @@
     1.4  fun if_debug f x = if !debug then f x else ()
     1.5  val message = if_debug writeln
     1.6  
     1.7 -(*Prints exceptions readably to users*)
     1.8 -fun print_sign_exn_unit sign e =
     1.9 -  case e of
    1.10 -     THM (msg,i,thms) =>
    1.11 -         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    1.12 -          List.app (writeln o Display.string_of_thm_global sign) thms)
    1.13 -   | THEORY (msg,thys) =>
    1.14 -         (writeln ("Exception THEORY raised:\n" ^ msg);
    1.15 -          List.app (writeln o Context.str_of_thy) thys)
    1.16 -   | TERM (msg,ts) =>
    1.17 -         (writeln ("Exception TERM raised:\n" ^ msg);
    1.18 -          List.app (writeln o Syntax.string_of_term_global sign) ts)
    1.19 -   | TYPE (msg,Ts,ts) =>
    1.20 -         (writeln ("Exception TYPE raised:\n" ^ msg);
    1.21 -          List.app (writeln o Syntax.string_of_typ_global sign) Ts;
    1.22 -          List.app (writeln o Syntax.string_of_term_global sign) ts)
    1.23 -   | e => raise e
    1.24 -
    1.25 -(*Prints an exception, then fails*)
    1.26 -fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
    1.27 -
    1.28  val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
    1.29  
    1.30  fun mk_meta_eq th =
    1.31 @@ -506,7 +485,6 @@
    1.32      in
    1.33          th
    1.34      end
    1.35 -    handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
    1.36  
    1.37  
    1.38  (* Closes a theorem with respect to free and schematic variables (does