# HG changeset patch
# User haftmann
# Date 1311278184 -7200
# Node ID 3406cd754dd28a783d3a3c867312ae417e4a3ef5
# Parent  78a0a2ad91a387d9f1ab5d09f1a5f42e722c0c46# Parent  481566bc20e43078519660de5212f8843dd8482b
merged

diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- 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,
diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- 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,
diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- 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
diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Tools/ATP/atp_translate.ML
--- 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
diff -r 481566bc20e4 -r 3406cd754dd2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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)