# HG changeset patch
# User bulwahn
# Date 1283248155 -7200
# Node ID 08eb0ffa24138af5f8d3c917cccb3e7367a4ae2b
# Parent  2eb265efa1b0220d0f441e4053d0e4f4776b10cd
improving clash-free naming of variables and preds in code_prolog

diff -r 2eb265efa1b0 -r 08eb0ffa2413 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 10:51:49 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 11:49:15 2010 +0200
@@ -84,9 +84,9 @@
 setup {* Code_Prolog.map_code_options (K 
   { ensure_groundness = true,
     limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
-    limited_predicates = [("typing", 2), ("nth_el1", 2)],
+    limited_predicates = [("typing", 2), ("nthel1", 2)],
     replacing = [(("typing", "limited_typing"), "quickcheck"),
-                 (("nth_el1", "limited_nth_el1"), "lim_typing")],
+                 (("nthel1", "limited_nthel1"), "lim_typing")],
     prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 lemma
diff -r 2eb265efa1b0 -r 08eb0ffa2413 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 10:51:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 11:49:15 2010 +0200
@@ -156,14 +156,14 @@
 
 (* translation from introduction rules to internal representation *)
 
-fun mk_conform empty avoid name =
+fun mk_conform f empty avoid name =
   let
     fun dest_Char (Symbol.Char c) = c
     val name' = space_implode "" (map (dest_Char o Symbol.decode)
       (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
         (Symbol.explode name)))
-    val name'' = if name' = "" then empty else name'
-  in Name.variant avoid name'' end
+    val name'' = f (if name' = "" then empty else name')
+  in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
 
 (** constant table **)
 
@@ -175,7 +175,7 @@
     fun update' c table =
       if AList.defined (op =) table c then table else
         let
-          val c' = first_lower (mk_conform "pred" (map snd table) (Long_Name.base_name c))
+          val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
         in
           AList.update (op =) (c, c') table
         end
@@ -282,7 +282,8 @@
         val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
         val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
       in clause end
-  in (map translate_intro intros', constant_table') end
+    val res = (map translate_intro intros', constant_table')
+  in res end
 
 fun depending_preds_of (key, intros) =
   fold Term.add_const_names (map Thm.prop_of intros) []
@@ -458,7 +459,7 @@
   forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
   
 fun mk_renaming v renaming =
-  (v, first_upper (mk_conform "var" (map snd renaming) v)) :: renaming
+  (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
 
 fun rename_vars_clause ((rel, args), prem) =
   let