--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Jul 21 18:40:31 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Jul 21 21:56:24 2011 +0200
@@ -79,7 +79,7 @@
section {* Manual setup to find counterexample *}
-setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
+setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Jul 21 18:40:31 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Jul 21 21:56:24 2011 +0200
@@ -5,7 +5,7 @@
"~~/src/HOL/Library/Code_Prolog"
begin
-setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
+setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Jul 21 18:40:31 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Jul 21 21:56:24 2011 +0200
@@ -2,11 +2,11 @@
"Examples",
"Predicate_Compile_Tests",
(* "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
- "Specialisation_Examples",
-(* "Hotel_Example_Small_Generator",*)
+ "Specialisation_Examples"
+(* "Hotel_Example_Small_Generator",
"IMP_1",
"IMP_2"
-(* "IMP_3",
+ "IMP_3",
"IMP_4"*)];
if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 21 18:40:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 21 21:56:24 2011 +0200
@@ -39,6 +39,7 @@
val const_prefix : string
val type_const_prefix : string
val class_prefix : string
+ val polymorphic_free_prefix : string
val skolem_const_prefix : string
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
@@ -125,8 +126,7 @@
val type_const_prefix = "tc_"
val class_prefix = "cl_"
-(* TODO: Use a more descriptive prefix in "SMT_Translate.lift_lambdas". *)
-val lambda_lifted_prefix = Name.uu
+val polymorphic_free_prefix = "poly_free"
val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
@@ -480,7 +480,7 @@
atyps_of T)
| iterm_from_term _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T,
- if String.isPrefix lambda_lifted_prefix s then [T] else []),
+ if String.isPrefix polymorphic_free_prefix s then [T] else []),
atyps_of T)
| iterm_from_term _ _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
@@ -1417,7 +1417,7 @@
if String.isPrefix skolem_const_prefix s then I
else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
| add (Free (s, T)) =
- if String.isPrefix lambda_lifted_prefix s then
+ if String.isPrefix polymorphic_free_prefix s then
T |> fold_type_constrs set_insert
else
I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 21 18:40:31 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 21 21:56:24 2011 +0200
@@ -541,7 +541,8 @@
rpair [] o map (conceal_lambdas ctxt)
else if trans = liftingN then
map (close_form o Envir.eta_contract) #> rpair ctxt
- #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier
+ #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
+ Lambda_Lifting.is_quantifier
#> fst
else if trans = combinatorsN then
rpair [] o map (introduce_combinators ctxt)