# HG changeset patch
# User obua
# Date 1126950569 -7200
# Node ID a389e5892691fee27bc1975ed217746e51d20d5f
# Parent  f503dccdff2783213f9871097db0e32743286aab
1) mapped .. and == constants
2) improved protect_varname

diff -r f503dccdff27 -r a389e5892691 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Sep 17 01:50:01 2005 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Sep 17 11:49:29 2005 +0200
@@ -41,6 +41,10 @@
   num > nat;
  (* sum > "+";*)
 
+const_renames
+  "==" > "eqeq"
+  ".." > "dotdot";
+
 const_maps
   T > True
   F > False
diff -r f503dccdff27 -r a389e5892691 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Sep 17 01:50:01 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Sep 17 11:49:29 2005 +0200
@@ -443,23 +443,29 @@
 	s |> no_quest |> beg_prime
     end
 
+val protected_varnames = ref (Symtab.empty:string Symtab.table)
+val invented_isavar = ref (IntInf.fromInt 0)
+
 fun protect_varname s =
-    let
-	fun no_beg_underscore s =
-	    if String.isPrefix "_" s
-	    then "dummy" ^ s
-	    else s
-    in
-	s |> no_beg_underscore
-    end
+    if Syntax.is_identifier s then s else
+    case Symtab.lookup (!protected_varnames) s of
+      SOME t => t
+    | NONE => 
+      let
+	  val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
+	  val t = "invented_isavar_"^(IntInf.toString (!invented_isavar))
+          val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
+      in
+	  t
+      end
 
-local
+(*local
   val sg = theory "Main"
 in
   fun is_valid_bound_varname s = (read_cterm sg ("SOME "^s^" . True", TypeInfer.logicT); true) handle _ => false
-end
+end*)
 
-fun protect_boundvarname s = if is_valid_bound_varname s then s else "u"
+fun protect_boundvarname s = if Syntax.is_identifier s then s else "u"
 
 fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
@@ -496,7 +502,10 @@
     tyn'
   end
 
-fun protect_constname tcn = implode (map (fn c => if c = "." then "_dot_" else c) (explode tcn))
+fun protect_constname tcn = tcn 
+ (* if tcn = ".." then "dotdot"
+  else if tcn = "==" then "eqeq"
+  else tcn*)
 
 structure TypeNet =
 struct