# HG changeset patch
# User paulson
# Date 865509701 -7200
# Node ID 9477a6410fe1a92c2e631c5c01c0fc671d1652b1
# Parent  862e153afc128bb244f7ede755f6f63757efeb71
Now extracts the predicate variable from induct0 insteead of trying to
predict its name.  The new "freeze" function requires this.

diff -r 862e153afc12 -r 9477a6410fe1 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Thu Jun 05 13:20:18 1997 +0200
+++ b/src/HOL/indrule.ML	Thu Jun 05 13:21:41 1997 +0200
@@ -213,20 +213,20 @@
 
 (** Uncurrying the predicate in the ordinary induction rule **)
 
-(*The name "x.1" comes from the "RS spec" !*)
-val xvar = cterm_of sign (Var(("x",1), elem_type));
+val xvar = cterm_of sign (Var(("x",0), elem_type));
 
 (*strip quantifier and instantiate the variable to a tuple*)
 val induct0 = quant_induct RS spec RSN (2,rev_mp) |>
+              zero_var_indexes |>
               freezeT |>     (*Because elem_type contains TFrees not TVars*)
               instantiate ([], [(xvar, cterm_of sign elem_tuple)]);
 
+val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
+
+
 in
   struct
-  val induct = standard 
-                  (Prod_Syntax.split_rule_var
-                    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
-                     induct0));
+  val induct = standard (Prod_Syntax.split_rule_var (pred_var, induct0));
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct = Prod_Syntax.remove_split mutual_induct_split