# HG changeset patch
# User bulwahn
# Date 1280417278 -7200
# Node ID 8c20eb9a388df2861d7136fb9059de26c35abb3a
# Parent  7fb011dd51de8c7cbc4b08d5b83201953877e0f1
cleaning example file; more natural ordering of variable names

diff -r 7fb011dd51de -r 8c20eb9a388d src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:57 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:58 2010 +0200
@@ -12,14 +12,6 @@
 
 code_pred append .
 
-ML {*
-  tracing (Code_Prolog.write_program (Code_Prolog.generate @{context} [@{const_name append}]))
-*}
-
-ML {*
-  Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"]
-*}
-
-values "{(x, y, z). append x y z}"
+values 3 "{((x::'b list), y, z). append x y z}"
 
 end
diff -r 7fb011dd51de -r 8c20eb9a388d src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:58 2010 +0200
@@ -283,7 +283,7 @@
     val (body, Ts, fp) = HOLogic.strip_psplits split;
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
-    val output_frees = map2 (curry Free) output_names (rev Ts)
+    val output_frees = rev (map2 (curry Free) output_names Ts)
     val body = subst_bounds (output_frees, body)
     val (pred as Const (name, T), all_args) =
       case strip_comb body of