# HG changeset patch
# User haftmann
# Date 1272446770 -7200
# Node ID d7cd6a5aa9c93060852935a3ca80105fff5bc347
# Parent  06081e4921d618fe374022c4ed0988d35408b22c
fix "fors" for proof of monotonicity

diff -r 06081e4921d6 -r d7cd6a5aa9c9 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Apr 28 08:25:02 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 28 11:26:10 2010 +0200
@@ -323,11 +323,11 @@
 
 (* prove monotonicity *)
 
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos ctxt =
  (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
     "  Proving monotonicity ...";
   (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
-    [] []
+    (map (fst o dest_Free) params) []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
@@ -689,7 +689,7 @@
       ||> Local_Theory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
+    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos lthy'';
     val ((_, [mono']), lthy''') =
       Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';