src/ZF/Tools/induct_tacs.ML
changeset 6112 5e4871c5136b
parent 6092 d9db67970c73
child 6141 a6922171b396
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Jan 13 11:56:28 1999 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jan 13 11:57:09 1999 +0100
     1.3 @@ -111,7 +111,9 @@
     1.4  	if exh then #exhaustion (datatype_info_sg sign tn)
     1.5  	       else #induct  (datatype_info_sg sign tn)
     1.6      val (Const("op :",_) $ Var(ixn,_) $ _) = 
     1.7 -	FOLogic.dest_Trueprop (hd (prems_of rule))
     1.8 +        (case prems_of rule of
     1.9 +	     [] => error "induction is not available for this datatype"
    1.10 +	   | major::_ => FOLogic.dest_Trueprop major)
    1.11      val ind_vname = Syntax.string_of_vname ixn
    1.12      val vname' = (*delete leading question mark*)
    1.13  	String.substring (ind_vname, 1, size ind_vname-1)
    1.14 @@ -139,9 +141,11 @@
    1.15  	map (head_of o const_of o FOLogic.dest_Trueprop o
    1.16  	     #prop o rep_thm) case_eqns;
    1.17  
    1.18 -    val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
    1.19 +    val Const ("op :", _) $ _ $ data =
    1.20  	FOLogic.dest_Trueprop (hd (prems_of elim));	
    1.21      
    1.22 +    val Const(big_rec_name, _) = head_of data;
    1.23 +
    1.24      val simps = case_eqns @ recursor_eqns;
    1.25  
    1.26      val dt_info =