equal
deleted
inserted
replaced
49 |
49 |
50 |
50 |
51 fun fundef_afterqed congs curry_info name data names atts thmss thy = |
51 fun fundef_afterqed congs curry_info name data names atts thmss thy = |
52 let |
52 let |
53 val (complete_thm :: compat_thms) = map hd thmss |
53 val (complete_thm :: compat_thms) = map hd thmss |
54 val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms) |
54 val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms) |
55 val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data |
55 val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data |
56 val Mutual {parts, ...} = curry_info |
56 val Mutual {parts, ...} = curry_info |
57 |
57 |
58 val Prep {names = Names {acc_R=accR, ...}, ...} = data |
58 val Prep {names = Names {acc_R=accR, ...}, ...} = data |
59 val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) |
59 val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) |