1.1 --- a/src/HOL/Import/proof_kernel.ML Fri Aug 28 18:23:24 2009 +0200
1.2 +++ b/src/HOL/Import/proof_kernel.ML Fri Aug 28 21:04:03 2009 +0200
1.3 @@ -199,12 +199,12 @@
1.4 val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
1.5 handle TERM _ => ct)
1.6 in
1.7 - quote(
1.8 + quote (
1.9 PrintMode.setmp [] (
1.10 Library.setmp show_brackets false (
1.11 Library.setmp show_all_types true (
1.12 Library.setmp Syntax.ambiguity_is_error false (
1.13 - Library.setmp show_sorts true Display.string_of_cterm))))
1.14 + Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
1.15 ct)
1.16 end
1.17
1.18 @@ -226,7 +226,8 @@
1.19 | G _ = raise SMART_STRING
1.20 fun F n =
1.21 let
1.22 - val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
1.23 + val str =
1.24 + Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
1.25 val u = Syntax.parse_term ctxt str
1.26 |> TypeInfer.constrain T |> Syntax.check_term ctxt
1.27 in
1.28 @@ -234,8 +235,9 @@
1.29 then quote str
1.30 else F (n+1)
1.31 end
1.32 - handle ERROR mesg => F (n+1)
1.33 - | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
1.34 + handle ERROR mesg => F (n + 1)
1.35 + | SMART_STRING =>
1.36 + error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
1.37 in
1.38 PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
1.39 end
1.40 @@ -243,8 +245,7 @@
1.41
1.42 val smart_string_of_thm = smart_string_of_cterm o cprop_of
1.43
1.44 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
1.45 -fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
1.46 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
1.47 fun prin t = writeln (PrintMode.setmp []
1.48 (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
1.49 fun pth (HOLThm(ren,thm)) =
1.50 @@ -1939,16 +1940,17 @@
1.51 then
1.52 let
1.53 val p1 = quotename constname
1.54 - val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
1.55 + val p2 = Syntax.string_of_typ_global thy'' ctype
1.56 val p3 = string_of_mixfix csyn
1.57 val p4 = smart_string_of_cterm crhs
1.58 in
1.59 - add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
1.60 + add_dump ("constdefs\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n " ^ p4) thy''
1.61 end
1.62 else
1.63 - (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
1.64 - "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
1.65 - thy'')
1.66 + add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
1.67 + Syntax.string_of_typ_global thy'' ctype ^
1.68 + "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n " ^
1.69 + quotename thmname ^ ": " ^ smart_string_of_cterm crhs) thy''
1.70 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
1.71 SOME (_,res) => HOLThm(rens_of linfo,res)
1.72 | NONE => raise ERR "new_definition" "Bad conclusion"
1.73 @@ -2008,8 +2010,9 @@
1.74 in
1.75 ((cname,cT,mk_syn thy cname)::cs,p)
1.76 end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
1.77 - val str = Library.foldl (fn (acc,(c,T,csyn)) =>
1.78 - acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
1.79 + val str = Library.foldl (fn (acc, (c, T, csyn)) =>
1.80 + acc ^ "\n " ^ quotename c ^ " :: \"" ^
1.81 + Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
1.82 val thy' = add_dump str thy
1.83 val _ = ImportRecorder.add_consts consts
1.84 in
1.85 @@ -2137,7 +2140,7 @@
1.86 fun add_dump_constdefs thy defname constname rhs ty =
1.87 let
1.88 val n = quotename constname
1.89 - val t = Display.string_of_ctyp (ctyp_of thy ty)
1.90 + val t = Syntax.string_of_typ_global thy ty
1.91 val syn = string_of_mixfix (mk_syn thy constname)
1.92 (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
1.93 val eq = quote (constname ^ " == "^rhs)
1.94 @@ -2224,7 +2227,7 @@
1.95 (" apply (rule light_ex_imp_nonempty[where t="^
1.96 (proc_prop (cterm_of thy4 t))^"])\n"^
1.97 (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
1.98 - val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
1.99 + val str_aty = Syntax.string_of_typ_global thy aty
1.100 val thy = add_dump_syntax thy rep_name
1.101 val thy = add_dump_syntax thy abs_name
1.102 val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^