src/HOL/Tools/datatype_aux.ML
changeset 18022 c1bb6480534f
parent 17485 c39871c52977
child 18069 f2c8f68a45e6
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Oct 28 22:27:44 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Oct 28 22:27:46 2005 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    (List.nth (prems_of st, i - 1)) of
     1.5      _ $ (_ $ (f $ x) $ (g $ y)) =>
     1.6        let
     1.7 -        val cong' = lift_rule (st, i) cong;
     1.8 +        val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong;
     1.9          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    1.10            Logic.strip_assums_concl (prop_of cong');
    1.11          val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
    1.12 @@ -151,7 +151,7 @@
    1.13      val prem = List.nth (prems_of state, i - 1);
    1.14      val params = Logic.strip_params prem;
    1.15      val (_, Type (tname, _)) = hd (rev params);
    1.16 -    val exhaustion = lift_rule (state, i) (exh_thm_of tname);
    1.17 +    val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname);
    1.18      val prem' = hd (prems_of exhaustion);
    1.19      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    1.20      val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),