equal
deleted
inserted
replaced
808 |> fold_map apply_theorems raw_distinct |
808 |> fold_map apply_theorems raw_distinct |
809 ||>> fold_map apply_theorems raw_inject |
809 ||>> fold_map apply_theorems raw_inject |
810 ||>> apply_theorems [raw_induction]; |
810 ||>> apply_theorems [raw_induction]; |
811 val sign = Theory.sign_of thy1; |
811 val sign = Theory.sign_of thy1; |
812 |
812 |
813 val ([induction'], _) = Variable.importT [induction] (Variable.thm_context induction); |
813 val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction); |
814 |
814 |
815 fun err t = error ("Ill-formed predicate in induction rule: " ^ |
815 fun err t = error ("Ill-formed predicate in induction rule: " ^ |
816 Sign.string_of_term sign t); |
816 Sign.string_of_term sign t); |
817 |
817 |
818 fun get_typ (t as _ $ Var (_, Type (tname, Ts))) = |
818 fun get_typ (t as _ $ Var (_, Type (tname, Ts))) = |