1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4  fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
     1.5    let
     1.6      val ((_, [induct']), _) =
     1.7 -      Variable.importT_thms [induct] (Variable.thm_context induct);
     1.8 +      Variable.importT [induct] (Variable.thm_context induct);
     1.9  
    1.10      fun err t = error ("Ill-formed predicate in induction rule: " ^
    1.11        Syntax.string_of_term_global thy t);