equal
deleted
inserted
replaced
32 |
32 |
33 val debug = Unsynchronized.ref false |
33 val debug = Unsynchronized.ref false |
34 |
34 |
35 fun if_debug f x = if !debug then f x else () |
35 fun if_debug f x = if !debug then f x else () |
36 val message = if_debug writeln |
36 val message = if_debug writeln |
37 |
|
38 (*Prints exceptions readably to users*) |
|
39 fun print_sign_exn_unit sign e = |
|
40 case e of |
|
41 THM (msg,i,thms) => |
|
42 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); |
|
43 List.app (writeln o Display.string_of_thm_global sign) thms) |
|
44 | THEORY (msg,thys) => |
|
45 (writeln ("Exception THEORY raised:\n" ^ msg); |
|
46 List.app (writeln o Context.str_of_thy) thys) |
|
47 | TERM (msg,ts) => |
|
48 (writeln ("Exception TERM raised:\n" ^ msg); |
|
49 List.app (writeln o Syntax.string_of_term_global sign) ts) |
|
50 | TYPE (msg,Ts,ts) => |
|
51 (writeln ("Exception TYPE raised:\n" ^ msg); |
|
52 List.app (writeln o Syntax.string_of_typ_global sign) Ts; |
|
53 List.app (writeln o Syntax.string_of_term_global sign) ts) |
|
54 | e => raise e |
|
55 |
|
56 (*Prints an exception, then fails*) |
|
57 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e) |
|
58 |
37 |
59 val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context; |
38 val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context; |
60 |
39 |
61 fun mk_meta_eq th = |
40 fun mk_meta_eq th = |
62 (case concl_of th of |
41 (case concl_of th of |
504 |> Thm.strip_shyps |
483 |> Thm.strip_shyps |
505 val _ = message ("norm_term: " ^ (string_of_thm th)) |
484 val _ = message ("norm_term: " ^ (string_of_thm th)) |
506 in |
485 in |
507 th |
486 th |
508 end |
487 end |
509 handle e => (writeln "norm_term internal error"; print_sign_exn thy e) |
|
510 |
488 |
511 |
489 |
512 (* Closes a theorem with respect to free and schematic variables (does |
490 (* Closes a theorem with respect to free and schematic variables (does |
513 not touch type variables, though). *) |
491 not touch type variables, though). *) |
514 |
492 |