# 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