src/HOL/Tools/datatype_package.ML
changeset 19841 f2fa72c13186
parent 19716 52c22fccdaaf
child 19874 cc4b2b882e4c
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Jun 11 19:36:10 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Jun 11 21:59:17 2006 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4  fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
     1.5    | prep_var _ = NONE;
     1.6  
     1.7 -fun prep_inst (concl, xs) =	(*exception UnequalLengths *)
     1.8 +fun prep_inst (concl, xs) =	(*exception Library.UnequalLengths *)
     1.9    let val vs = InductAttrib.vars_of concl
    1.10    in List.mapPartial prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.11  
    1.12 @@ -199,7 +199,7 @@
    1.13  	    in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) 
    1.14  	    end
    1.15      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.16 -    val insts = List.concat (map prep_inst (concls ~~ varss)) handle UnequalLengths =>
    1.17 +    val insts = List.concat (map prep_inst (concls ~~ varss)) handle Library.UnequalLengths =>
    1.18        error (rule_name ^ " has different numbers of variables");
    1.19    in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
    1.20    i state;