# HG changeset patch
# User haftmann
# Date 1272459257 -7200
# Node ID ade0dee3a58e156b18a0e0d2e96af64fd9f5ba2d
# Parent  0e2300856d7d5896bb13e5d4731d2ccaf32e4c63# Parent  d7cd6a5aa9c93060852935a3ca80105fff5bc347
merged

diff -r 0e2300856d7d -r ade0dee3a58e src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Apr 28 14:01:54 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 28 14:54:17 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'';