equal
deleted
inserted
replaced
40 fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions dtor_corec_transfers |
40 fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions dtor_corec_transfers |
41 rel_pre_defs disc_eq_cases cases case_distribs case_congs = |
41 rel_pre_defs disc_eq_cases cases case_distribs case_congs = |
42 let |
42 let |
43 fun instantiate_with_lambda thm = |
43 fun instantiate_with_lambda thm = |
44 let |
44 let |
45 val prop as @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) = |
45 val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) = |
46 Thm.prop_of thm; |
46 Thm.prop_of thm; |
47 val T = range_type fT; |
47 val T = range_type fT; |
48 val j = Term.maxidx_of_term prop + 1; |
48 val j = Term.maxidx_of_term prop + 1; |
49 val cond = Var (("x", j), HOLogic.boolT); |
49 val cond = Var (("x", j), HOLogic.boolT); |
50 val then_branch = Var (("t", j), T); |
50 val then_branch = Var (("t", j), T); |