--- a/src/HOL/Import/proof_kernel.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sat Oct 17 15:57:51 2009 +0200
@@ -201,10 +201,10 @@
in
quote (
PrintMode.setmp [] (
- Library.setmp show_brackets false (
- Library.setmp show_all_types true (
- Library.setmp Syntax.ambiguity_is_error false (
- Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
+ setmp_CRITICAL show_brackets false (
+ setmp_CRITICAL show_all_types true (
+ setmp_CRITICAL Syntax.ambiguity_is_error false (
+ setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
ct)
end
@@ -219,15 +219,15 @@
val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
fun match u = t aconv u
- fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
- | G 1 = Library.setmp show_brackets true (G 0)
- | G 2 = Library.setmp show_all_types true (G 0)
- | G 3 = Library.setmp show_brackets true (G 2)
+ fun G 0 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)
+ | G 1 = setmp_CRITICAL show_brackets true (G 0)
+ | G 2 = setmp_CRITICAL show_all_types true (G 0)
+ | G 3 = setmp_CRITICAL show_brackets true (G 2)
| G _ = raise SMART_STRING
fun F n =
let
val str =
- Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
+ setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
val u = Syntax.parse_term ctxt str
|> TypeInfer.constrain T |> Syntax.check_term ctxt
in
@@ -239,7 +239,7 @@
| SMART_STRING =>
error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
in
- PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
+ PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
end
handle ERROR mesg => simple_smart_string_of_cterm ct
@@ -2124,7 +2124,7 @@
else "(" ^ commas tnames ^ ") "
val proc_prop = if null tnames
then smart_string_of_cterm
- else Library.setmp show_all_types true smart_string_of_cterm
+ else setmp_CRITICAL show_all_types true smart_string_of_cterm
val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
@@ -2219,7 +2219,7 @@
else "(" ^ commas tnames ^ ") "
val proc_prop = if null tnames
then smart_string_of_cterm
- else Library.setmp show_all_types true smart_string_of_cterm
+ else setmp_CRITICAL show_all_types true smart_string_of_cterm
val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
" = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
(string_of_mixfix tsyn) ^ " morphisms "^