# HG changeset patch
# User bulwahn
# Date 1280650543 -7200
# Node ID 561aa8eb63d3777ef678bc2ede9ec319685b91b2
# Parent  5ae05823cfd9b2b31d1d010a9681333bdfff0a71
inductive_simps learns to have more tool compliance

diff -r 5ae05823cfd9 -r 561aa8eb63d3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Aug 01 10:15:43 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun Aug 01 10:15:43 2010 +0200
@@ -548,15 +548,18 @@
 
 fun mk_simp_eq ctxt prop =
   let
-    val (c, args) = strip_comb (HOLogic.dest_Trueprop prop)
     val ctxt' = Variable.auto_fixes prop ctxt
-    val cname = fst (dest_Const c)
+    val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
     val info = the_inductive ctxt cname
     val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
-    val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))))
+    val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
+    val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
+      (Vartab.empty, Vartab.empty)
     val certify = cterm_of (ProofContext.theory_of ctxt)
-  in
-    cterm_instantiate (map (pairself certify) (args' ~~ args)) eq
+    val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
+      (Term.add_vars lhs_eq [])
+   in
+    cterm_instantiate inst eq
     |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
       (Simplifier.full_rewrite (simpset_of ctxt))))
     |> singleton (Variable.export ctxt' ctxt)