equal
deleted
inserted
replaced
188 | G 1 = Library.setmp show_types true |
188 | G 1 = Library.setmp show_types true |
189 | G 2 = Library.setmp show_all_types true |
189 | G 2 = Library.setmp show_all_types true |
190 | G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct)) |
190 | G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct)) |
191 fun F sh_br n = |
191 fun F sh_br n = |
192 let |
192 let |
193 val str = Library.setmp show_brackets sh_br (G n string_of_cterm) ct |
193 val str = Library.setmp show_brackets sh_br (G n (Output.output o string_of_cterm)) ct |
194 val cu = transform_error (read_cterm sign) (str,T) |
194 val cu = transform_error (read_cterm sign) (str,T) |
195 in |
195 in |
196 if match cu |
196 if match cu |
197 then quote str |
197 then quote str |
198 else F false (n+1) |
198 else F false (n+1) |
206 transform_error (Library.setmp Syntax.ambiguity_is_error true (F false)) 0 |
206 transform_error (Library.setmp Syntax.ambiguity_is_error true (F false)) 0 |
207 end |
207 end |
208 handle ERROR_MESSAGE mesg => |
208 handle ERROR_MESSAGE mesg => |
209 (writeln "Exception in smart_string_of_cterm!"; |
209 (writeln "Exception in smart_string_of_cterm!"; |
210 writeln mesg; |
210 writeln mesg; |
211 quote (string_of_cterm ct)) |
211 quote (Output.output (string_of_cterm ct))) |
212 |
212 |
213 val smart_string_of_thm = smart_string_of_cterm o cprop_of |
213 val smart_string_of_thm = smart_string_of_cterm o cprop_of |
214 |
214 |
215 fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th) |
215 fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th) |
216 fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct) |
216 fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct) |
1896 val sg = sign_of thy'' |
1896 val sg = sign_of thy'' |
1897 val rew = rewrite_hol4_term eq thy'' |
1897 val rew = rewrite_hol4_term eq thy'' |
1898 val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew))) |
1898 val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew))) |
1899 val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn |
1899 val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn |
1900 then |
1900 then |
1901 add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg ctype)) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy'' |
1901 add_dump ("constdefs\n " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n " ^ (smart_string_of_cterm crhs)) thy'' |
1902 else |
1902 else |
1903 add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg ctype)) ^ |
1903 add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^ |
1904 "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) |
1904 "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) |
1905 thy'' |
1905 thy'' |
1906 |
1906 |
1907 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of |
1907 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of |
1908 Some (_,res) => HOLThm(rens_of linfo,res) |
1908 Some (_,res) => HOLThm(rens_of linfo,res) |
1962 in |
1962 in |
1963 ((cname,cT,mk_syn thy cname)::cs,p) |
1963 ((cname,cT,mk_syn thy cname)::cs,p) |
1964 end) (([],HOLogic.dest_Trueprop (concl_of th)),names) |
1964 end) (([],HOLogic.dest_Trueprop (concl_of th)),names) |
1965 val sg = sign_of thy |
1965 val sg = sign_of thy |
1966 val str = foldl (fn (acc,(c,T,csyn)) => |
1966 val str = foldl (fn (acc,(c,T,csyn)) => |
1967 acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts) |
1967 acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts) |
1968 val thy' = add_dump str thy |
1968 val thy' = add_dump str thy |
1969 in |
1969 in |
1970 Theory.add_consts_i consts thy' |
1970 Theory.add_consts_i consts thy' |
1971 end |
1971 end |
1972 |
1972 |