# HG changeset patch
# User paulson
# Date 865509336 -7200
# Node ID dfd9cbad5530f29b6f87eef9d7a0726f4f19f5dd
# Parent  3e2b8d0de2a07ac5562498520a74e251521615f2
Now extracts the predicate variable from induct0 insteead of trying to
predict its name

diff -r 3e2b8d0de2a0 -r dfd9cbad5530 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Thu Jun 05 13:14:52 1997 +0200
+++ b/src/ZF/indrule.ML	Thu Jun 05 13:15:36 1997 +0200
@@ -234,14 +234,13 @@
 (*strip quantifier and the implication*)
 val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
 
+val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
 
 in
   struct
   (*strip quantifier*)
-  val induct = standard 
-                  (CP.split_rule_var
-                    (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
-                     induct0));
+  val induct = CP.split_rule_var(pred_var, elem_type-->Ind_Syntax.oT, induct0) 
+               |> standard;
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct = CP.remove_split mutual_induct_fsplit