equal
deleted
inserted
replaced
85 else raise Match |
85 else raise Match |
86 val _ = if !trace then |
86 val _ = if !trace then |
87 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) |
87 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) |
88 else (); |
88 else (); |
89 val goal = Logic.mk_equals (old, new) |
89 val goal = Logic.mk_equals (old, new) |
90 val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN |
90 val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN |
91 simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) |
91 simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) |
92 handle ERROR_MESSAGE msg => |
92 handle ERROR_MESSAGE msg => |
93 (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal); |
93 (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal); |
94 raise Match) |
94 raise Match) |
95 in SOME thm end |
95 in SOME thm end |