src/HOL/Import/proof_kernel.ML
changeset 32966 5b21661fe618
parent 32951 83392f9d303f
child 33035 15eab423e573
child 33037 b22e44496dc2
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Oct 17 15:55:57 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Oct 17 15:57:51 2009 +0200
     1.3 @@ -201,10 +201,10 @@
     1.4      in
     1.5          quote (
     1.6          PrintMode.setmp [] (
     1.7 -        Library.setmp show_brackets false (
     1.8 -        Library.setmp show_all_types true (
     1.9 -        Library.setmp Syntax.ambiguity_is_error false (
    1.10 -        Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
    1.11 +        setmp_CRITICAL show_brackets false (
    1.12 +        setmp_CRITICAL show_all_types true (
    1.13 +        setmp_CRITICAL Syntax.ambiguity_is_error false (
    1.14 +        setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
    1.15          ct)
    1.16      end
    1.17  
    1.18 @@ -219,15 +219,15 @@
    1.19          val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    1.20                     handle TERM _ => ct)
    1.21          fun match u = t aconv u
    1.22 -        fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
    1.23 -          | G 1 = Library.setmp show_brackets true (G 0)
    1.24 -          | G 2 = Library.setmp show_all_types true (G 0)
    1.25 -          | G 3 = Library.setmp show_brackets true (G 2)
    1.26 +        fun G 0 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)
    1.27 +          | G 1 = setmp_CRITICAL show_brackets true (G 0)
    1.28 +          | G 2 = setmp_CRITICAL show_all_types true (G 0)
    1.29 +          | G 3 = setmp_CRITICAL show_brackets true (G 2)
    1.30            | G _ = raise SMART_STRING
    1.31          fun F n =
    1.32              let
    1.33                  val str =
    1.34 -                  Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
    1.35 +                  setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
    1.36                  val u = Syntax.parse_term ctxt str
    1.37                    |> TypeInfer.constrain T |> Syntax.check_term ctxt
    1.38              in
    1.39 @@ -239,7 +239,7 @@
    1.40                | SMART_STRING =>
    1.41                    error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
    1.42      in
    1.43 -      PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    1.44 +      PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    1.45      end
    1.46      handle ERROR mesg => simple_smart_string_of_cterm ct
    1.47  
    1.48 @@ -2124,7 +2124,7 @@
    1.49                                  else "(" ^ commas tnames ^ ") "
    1.50              val proc_prop = if null tnames
    1.51                              then smart_string_of_cterm
    1.52 -                            else Library.setmp show_all_types true smart_string_of_cterm
    1.53 +                            else setmp_CRITICAL show_all_types true smart_string_of_cterm
    1.54              val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
    1.55                                   ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
    1.56  
    1.57 @@ -2219,7 +2219,7 @@
    1.58                                  else "(" ^ commas tnames ^ ") "
    1.59              val proc_prop = if null tnames
    1.60                              then smart_string_of_cterm
    1.61 -                            else Library.setmp show_all_types true smart_string_of_cterm
    1.62 +                            else setmp_CRITICAL show_all_types true smart_string_of_cterm
    1.63              val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
    1.64                " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
    1.65                (string_of_mixfix tsyn) ^ " morphisms "^