# HG changeset patch
# User bulwahn
# Date 1288034236 -7200
# Node ID 128f8a1611e6a0fcdafe53ddbb29636e65c07b69
# Parent  0e8a4e27a685c5444784809e86baea4416d0989f
relaxing the filtering condition for getting specifications from Spec_Rules

diff -r 0e8a4e27a685 -r 128f8a1611e6 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Oct 25 21:17:16 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Oct 25 21:17:16 2010 +0200
@@ -74,6 +74,11 @@
 *)
 val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
 
+fun defining_const_of_introrule th =
+  case defining_term_of_introrule th
+   of Const (c, _) => c
+    | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+
 (*TODO*)
 fun is_introlike_term t = true
 
@@ -194,7 +199,7 @@
         defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
         SOME (normalize_equation thy th)
       else
-        if is_introlike th andalso defining_term_of_introrule th = t then
+        if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
           SOME th
         else
           NONE
@@ -206,7 +211,8 @@
     | ths => rev ths
     val _ =
       if show_intermediate_results options then
-        Output.tracing (commas (map (Display.string_of_thm_global thy) spec))
+        Output.tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
+          commas (map (Display.string_of_thm_global thy) spec))
       else ()
   in
     spec