equal
deleted
inserted
replaced
265 let |
265 let |
266 val T = fastype_of t; |
266 val T = fastype_of t; |
267 val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); |
267 val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); |
268 val cname = case chead_of t of Const(c,_) => c | _ => |
268 val cname = case chead_of t of Const(c,_) => c | _ => |
269 fixrec_err "function is not declared as constant in theory"; |
269 fixrec_err "function is not declared as constant in theory"; |
270 val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold")); |
270 val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE)); |
271 val simp = Goal.prove_global thy [] [] eq |
271 val simp = Goal.prove_global thy [] [] eq |
272 (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); |
272 (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); |
273 in simp end; |
273 in simp end; |
274 |
274 |
275 fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = |
275 fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = |