# HG changeset patch
# User bulwahn
# Date 1272476769 -7200
# Node ID 875218f3f97cb13526e977c6da1f6c3dd1946018
# Parent  db2953f5887af99c6aca9a407da013324006468e# Parent  6c7ba330ab42bf28857570273b23198af903d696
merged

diff -r 6c7ba330ab42 -r 875218f3f97c src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 28 19:43:45 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 28 19:46:09 2010 +0200
@@ -686,6 +686,13 @@
 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
 
+subsection {* Free function variable *}
+
+inductive FF :: "nat => nat => bool"
+where
+  "f x = y ==> FF x y"
+
+code_pred FF .
 
 subsection {* IMP *}
 
diff -r 6c7ba330ab42 -r 875218f3f97c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 28 19:43:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 28 19:46:09 2010 +0200
@@ -529,16 +529,19 @@
     fun instantiate i n {context = ctxt, params = p, prems = prems,
       asms = a, concl = cl, schematics = s}  =
       let
+        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
+        fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
+          |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
         val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
         val case_th = MetaSimplifier.simplify true
-        (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs)
-          (nth cases (i - 1))
+          (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
         val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
         val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
-        val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty)
-        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
-        val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
-        val thesis = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl}) OF prems'
+        val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
+          OF (replicate nargs @{thm refl})
+        val thesis =
+          Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
+            OF prems'
       in
         (rtac thesis 1)
       end