Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now extracts the predicate variable from induct0 insteead of trying to
authorpaulson
Thu, 05 Jun 1997 13:15:36 +0200
changeset 3398 dfd9cbad5530
parent 3397 3e2b8d0de2a0
child 3399 0c4efa9eac29
Now extracts the predicate variable from induct0 insteead of trying to predict its name
src/ZF/indrule.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle