src/HOL/Import/proof_kernel.ML
changeset 26928 ca87aff1ad2d
parent 26626 c6231d64d264
child 26939 1035c89b4c02
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4          Library.setmp show_brackets false (
     1.5          Library.setmp show_all_types true (
     1.6          Library.setmp Syntax.ambiguity_is_error false (
     1.7 -        Library.setmp show_sorts true string_of_cterm))))
     1.8 +        Library.setmp show_sorts true Display.string_of_cterm))))
     1.9          ct)
    1.10      end
    1.11  
    1.12 @@ -227,7 +227,7 @@
    1.13            | G _ = raise SMART_STRING
    1.14          fun F n =
    1.15              let
    1.16 -                val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    1.17 +                val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
    1.18                  val u = Syntax.parse_term ctxt str
    1.19                    |> TypeInfer.constrain T |> Syntax.check_term ctxt
    1.20              in
    1.21 @@ -236,7 +236,7 @@
    1.22                  else F (n+1)
    1.23              end
    1.24              handle ERROR mesg => F (n+1)
    1.25 -                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
    1.26 +                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
    1.27      in
    1.28        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    1.29      end
    1.30 @@ -244,8 +244,8 @@
    1.31  
    1.32  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    1.33  
    1.34 -fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
    1.35 -fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct)
    1.36 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
    1.37 +fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
    1.38  fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
    1.39  fun pth (HOLThm(ren,thm)) =
    1.40      let
    1.41 @@ -1947,14 +1947,14 @@
    1.42                      then
    1.43                          let
    1.44                              val p1 = quotename constname
    1.45 -                            val p2 = string_of_ctyp (ctyp_of thy'' ctype)
    1.46 +                            val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
    1.47                              val p3 = string_of_mixfix csyn
    1.48                              val p4 = smart_string_of_cterm crhs
    1.49                          in
    1.50                              add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
    1.51                          end
    1.52                      else
    1.53 -                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
    1.54 +                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
    1.55                                     "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
    1.56                                    thy'')
    1.57          val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
    1.58 @@ -2017,7 +2017,7 @@
    1.59                                                                ((cname,cT,mk_syn thy cname)::cs,p)
    1.60                                                            end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
    1.61                                 val str = Library.foldl (fn (acc,(c,T,csyn)) =>
    1.62 -                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
    1.63 +                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
    1.64                                 val thy' = add_dump str thy
    1.65                                 val _ = ImportRecorder.add_consts consts
    1.66                             in
    1.67 @@ -2143,7 +2143,7 @@
    1.68  fun add_dump_constdefs thy defname constname rhs ty =
    1.69      let
    1.70          val n = quotename constname
    1.71 -        val t = string_of_ctyp (ctyp_of thy ty)
    1.72 +        val t = Display.string_of_ctyp (ctyp_of thy ty)
    1.73          val syn = string_of_mixfix (mk_syn thy constname)
    1.74          (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
    1.75          val eq = quote (constname ^ " == "^rhs)
    1.76 @@ -2228,7 +2228,7 @@
    1.77                ("  apply (rule light_ex_imp_nonempty[where t="^
    1.78                (proc_prop (cterm_of thy4 t))^"])\n"^
    1.79                ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
    1.80 -            val str_aty = string_of_ctyp (ctyp_of thy aty)
    1.81 +            val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
    1.82              val thy = add_dump_syntax thy rep_name
    1.83              val thy = add_dump_syntax thy abs_name
    1.84              val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^