# 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