higher-order arguments in different rules are fixed to one name in the predicate compiler

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -258,23 +258,33 @@
 
 (* generation of case rules from user-given introduction rules *)
 
+(* how to detect polymorphic type dependencies in mutual recursive inductive predicates? *)
 fun import_intros [] ctxt = ([], ctxt)
   | import_intros (th :: ths) ctxt =
     let
       val ((_, [th']), ctxt') = Variable.import false [th] ctxt
-      val (pred, _) = strip_intro_concl 0 (prop_of th')
+      val thy = ProofContext.theory_of ctxt'
+      val (pred, ([], args)) = strip_intro_concl 0 (prop_of th')
+      val ho_args = filter (is_predT o fastype_of) args
       fun instantiate_typ th =
         let
           val (pred', _) = strip_intro_concl 0 (prop_of th)
-          val subst = Sign.typ_match (ProofContext.theory_of ctxt')
+          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+            error "Trying to instantiate another predicate" else ()
+          val subst = Sign.typ_match thy
             (fastype_of pred', fastype_of pred) Vartab.empty
           val _ = Output.tracing (commas (map (fn ((x, i), (s, T)) => x ^ " instantiate to " ^ (Syntax.string_of_typ ctxt' T))
           (Vartab.dest subst)))
           val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T))
             (Vartab.dest subst)
         in Thm.certify_instantiate (subst', []) th end;
+      fun instantiate_ho_args th =
+        let
+          val (_, (_, args')) = strip_intro_concl 0 (prop_of th)
+          val ho_args' = map dest_Var (filter (is_predT o fastype_of) args')
+        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
       val ((_, ths'), ctxt1) =
-        Variable.import false (map instantiate_typ ths) ctxt'
+        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
     in
       (th' :: ths', ctxt1)
     end

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -446,7 +446,7 @@
 code_pred (inductify_all) S\<^isub>1p .
 
 thm S\<^isub>1p.equation
-(*
+
 theorem S\<^isub>1_sound:
 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 quickcheck[generator=pred_compile]
@@ -477,9 +477,8 @@
 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
 
-(*
 code_pred (inductify_all) S\<^isub>3 .
-*)
+
 theorem S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 quickcheck[generator=pred_compile, size=10, iterations=1]
@@ -488,7 +487,7 @@
 lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
 quickcheck[size=10, generator = pred_compile]
 oops
-*)
+
 inductive test
 where
   "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] ==> test w"