src/HOL/Tools/datatype_package.ML
changeset 22598 f31a869077f0
parent 22578 b0eb5652f210
child 22675 acf10be7dcca
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Apr 04 23:29:37 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 04 23:29:38 2007 +0200
     1.3 @@ -195,8 +195,8 @@
     1.4            SOME r => (r, "Induction rule")
     1.5          | NONE =>
     1.6              let val tn = find_tname (hd (map_filter I (flat varss))) Bi
     1.7 -                val {sign, ...} = Thm.rep_thm state
     1.8 -            in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) 
     1.9 +                val thy = Thm.theory_of_thm state
    1.10 +            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn) 
    1.11              end
    1.12      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.13      val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    1.14 @@ -825,7 +825,8 @@
    1.15        ||>> fold_map apply_theorems raw_inject
    1.16        ||>> apply_theorems [raw_induction];
    1.17  
    1.18 -    val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
    1.19 +    val ((_, [induction']), _) =
    1.20 +      Variable.importT_thms [induction] (Variable.thm_context induction);
    1.21  
    1.22      fun err t = error ("Ill-formed predicate in induction rule: " ^
    1.23        Sign.string_of_term thy1 t);