equal
deleted
inserted
replaced
797 |> fold_map apply_theorems raw_distinct |
797 |> fold_map apply_theorems raw_distinct |
798 ||>> fold_map apply_theorems raw_inject |
798 ||>> fold_map apply_theorems raw_inject |
799 ||>> apply_theorems [raw_induction]; |
799 ||>> apply_theorems [raw_induction]; |
800 val sign = Theory.sign_of thy1; |
800 val sign = Theory.sign_of thy1; |
801 |
801 |
802 val induction' = Thm.freezeT induction; |
802 val ([induction'], _) = Variable.importT [induction] (Variable.thm_context induction); |
803 |
803 |
804 fun err t = error ("Ill-formed predicate in induction rule: " ^ |
804 fun err t = error ("Ill-formed predicate in induction rule: " ^ |
805 Sign.string_of_term sign t); |
805 Sign.string_of_term sign t); |
806 |
806 |
807 fun get_typ (t as _ $ Var (_, Type (tname, Ts))) = |
807 fun get_typ (t as _ $ Var (_, Type (tname, Ts))) = |