# HG changeset patch
# User urbanc
# Date 1131356845 -3600
# Node ID e956b04fea221cbd7e7a40ba443d09fca842a09e
# Parent  227ecb2cfa3d7943d61b80e8115d464c283a6492
fixed bug with nominal induct
- the bug occured in rule inductions when
  the goal did not use all variables from
  the relation over which the induction
  was done

diff -r 227ecb2cfa3d -r e956b04fea22 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon Nov 07 09:34:51 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Mon Nov 07 10:47:25 2005 +0100
@@ -21,7 +21,7 @@
 
 fun find_var frees name =
   (case Library.find_first (equal name o fst o dest_Free) frees of
-    NONE => error ("No such Variable in term: " ^ quote name)
+    NONE =>   error ("No such Variable in term: " ^ quote name) 
   | SOME v => v);
 
 (* - names specifies the variables that are involved in the *)
@@ -31,10 +31,16 @@
   let
     val sg     = Thm.sign_of_thm state;
     val cert   = Thm.cterm_of sg;
+
+    val facts1 = Library.take (1, facts);
+    val facts2 = Library.drop (1, facts);
+
     val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
-    val frees  = Term.term_frees goal;
+    val frees  = foldl Term.add_term_frees [] (goal :: map concl_of facts1);
     val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
-    val vars = map (find_var frees) names;
+    val vars = map (find_var frees) names; 
+                 (* FIXME - check what one can do in case of *)
+                 (* rule inductions                          *)
 
     fun inst_rule rule =
       let
@@ -53,9 +59,6 @@
       Simplifier.full_simplify (HOL_basic_ss addsimps
         [split_conv, split_paired_All, split_paired_all]);
 
-    val facts1 = Library.take (1, facts);
-    val facts2 = Library.drop (1, facts);
-
   in
     rule
     |> inst_rule