equal
deleted
inserted
replaced
27 struct |
27 struct |
28 |
28 |
29 val trace = Unsynchronized.ref false; |
29 val trace = Unsynchronized.ref false; |
30 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
30 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
31 |
31 |
32 (* FIXME legacy *) |
32 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th); |
33 fun freeze_thm th = #1 (Drule.freeze_thaw th); |
|
34 |
33 |
35 fun type_has_empty_sort (TFree (_, [])) = true |
34 fun type_has_empty_sort (TFree (_, [])) = true |
36 | type_has_empty_sort (TVar (_, [])) = true |
35 | type_has_empty_sort (TVar (_, [])) = true |
37 | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts |
36 | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts |
38 | type_has_empty_sort _ = false; |
37 | type_has_empty_sort _ = false; |