src/HOL/Tools/Predicate_Compile/code_prolog.ML

--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
@@ -234,19 +234,14 @@
 
 fun generate options ctxt const =
   let 
-    val T = Sign.the_const_type (ProofContext.theory_of ctxt) const
-    val t = Const (const, T)
-    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
-    val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
-    val ctxt'' = ProofContext.init_global thy'
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
-    val gr = Predicate_Compile_Core.intros_graph_of ctxt''
+    val gr = Predicate_Compile_Core.intros_graph_of ctxt
     val gr' = add_edges depending_preds_of const gr
     val scc = strong_conn_of gr' [const]
     val constant_table = mk_constant_table (flat scc)
   in
-    apfst flat (fold_map (translate_intros options ctxt'' gr) (flat scc) constant_table)
+    apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
   end
   
 (* add implementation for ground predicates *)
@@ -458,9 +453,15 @@
       case try (map (fst o dest_Free)) all_args of
         SOME vs => vs
       | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
+    val _ = tracing "Preprocessing specification..."
+    val T = Sign.the_const_type (ProofContext.theory_of ctxt) name
+    val t = Const (name, T)
+    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
+    val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
+    val ctxt'' = ProofContext.init_global thy'
     val _ = tracing "Generating prolog program..."
-    val (p, constant_table) = generate options ctxt name
-      |> (if #ensure_groundness options then add_ground_predicates ctxt else I)
+    val (p, constant_table) = generate options ctxt'' name
+      |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I)
     val _ = tracing "Running prolog program..."
     val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
     val _ = tracing "Restoring terms..."
@@ -478,7 +479,7 @@
             mk_set_compr (t :: in_insert) ts xs
           else
             let
-              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
+              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt'' [t]) ("uu", fastype_of t)
               val set_compr =
                 HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
                   frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
@@ -489,7 +490,7 @@
         end
   in
       foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
-        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts))) tss) [])
+        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt'' constant_table) (ts ~~ Ts))) tss) [])
   end
 
 fun values_cmd print_modes soln raw_t state =
@@ -516,4 +517,5 @@
    >> (fn ((print_modes, soln), t) => Toplevel.keep
         (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
 
+
 end;