# HG changeset patch # User wenzelm # Date 1302950778 -7200 # Node ID 3305f573294ebf4ca7451b932b45ccd0f8744d55 # Parent e8777e3ea6ef3ae5c47d9d34709910164fce0f2f tuned signature, disentangled dependencies; diff -r e8777e3ea6ef -r 3305f573294e src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Apr 16 12:46:18 2011 +0200 @@ -51,7 +51,7 @@ fun sanity_test NONE _ = true | sanity_test (SOME bind) str = - if Name.of_binding bind = str then true + if Variable.name bind = str then true else error_msg bind str val _ = sanity_test optbind lhs_str diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/class_declaration.ML Sat Apr 16 12:46:18 2011 +0200 @@ -255,7 +255,7 @@ thy |> Sign.declare_const ((b, ty0), syn) |> snd - |> pair ((Name.of_binding b, ty), (c, ty')) + |> pair ((Variable.name b, ty), (c, ty')) end; in thy diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/element.ML Sat Apr 16 12:46:18 2011 +0200 @@ -99,7 +99,7 @@ fun map_ctxt {binding, typ, term, pattern, fact, attrib} = fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) | Constrains xs => Constrains (xs |> map (fn (x, T) => - (Name.of_binding (binding (Binding.name x)), typ T))) + (Variable.name (binding (Binding.name x)), typ T))) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => @@ -526,7 +526,7 @@ fun activate raw_elem ctxt = let val elem = raw_elem |> map_ctxt - {binding = tap Name.of_binding, + {binding = tap Variable.name, typ = I, term = I, pattern = I, diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/expression.ML Sat Apr 16 12:46:18 2011 +0200 @@ -128,7 +128,7 @@ val (implicit, expr') = params_expr expr; val implicit' = map #1 implicit; - val fixed' = map (#1 #> Name.of_binding) fixed; + val fixed' = map (Variable.name o #1) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] @@ -395,7 +395,7 @@ val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5); (* Retrieve parameter types *) - val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes) + val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes) | _ => fn ps => ps) (Fixes fors :: elems') []; val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; val parms = xs ~~ Ts; (* params from expression and elements *) diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/local_defs.ML Sat Apr 16 12:46:18 2011 +0200 @@ -92,7 +92,7 @@ let val ((bvars, mxs), specs) = defs |> split_list |>> split_list; val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; - val xs = map Name.of_binding bvars; + val xs = map Variable.name bvars; val names = map2 Thm.def_binding_optional bvars bfacts; val eqs = mk_def ctxt (xs ~~ rhss); val lhss = map (fst o Logic.dest_equals) eqs; diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/obtain.ML Sat Apr 16 12:46:18 2011 +0200 @@ -119,7 +119,7 @@ (*obtain vars*) val (vars, vars_ctxt) = prep_vars raw_vars ctxt; val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars; - val xs = map (Name.of_binding o #1) vars; + val xs = map (Variable.name o #1) vars; (*obtain asms*) val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); @@ -257,7 +257,7 @@ fun inferred_type (binding, _, mx) ctxt = let - val x = Name.of_binding binding; + val x = Variable.name binding; val (T, ctxt') = ProofContext.inferred_param x ctxt in ((x, T, mx), ctxt') end; diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat Apr 16 12:46:18 2011 +0200 @@ -923,7 +923,7 @@ fun prep_vars prep_typ internal = fold_map (fn (b, raw_T, mx) => fn ctxt => let - val x = Name.of_binding b; + val x = Variable.name b; val _ = Lexicon.is_identifier (no_skolem internal x) orelse error ("Illegal variable name: " ^ quote (Binding.str_of b)); @@ -1023,7 +1023,7 @@ fun add_fixes raw_vars ctxt = let val (vars, _) = cert_vars raw_vars ctxt; - val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt; + val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt; val ctxt'' = ctxt' |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) diff -r e8777e3ea6ef -r 3305f573294e src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/Isar/specification.ML Sat Apr 16 12:46:18 2011 +0200 @@ -172,7 +172,7 @@ fun gen_axioms do_print prep raw_vars raw_specs thy = let val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy); - val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars; + val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars; (*consts*) val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars; @@ -182,7 +182,7 @@ val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) => fold_map Thm.add_axiom (map (apfst (fn a => Binding.map_name (K a) b)) - (Global_Theory.name_multi (Name.of_binding b) (map subst props))) + (Global_Theory.name_multi (Variable.name b) (map subst props))) #>> (fn ths => ((b, atts), [(map #2 ths, [])]))); (*facts*) @@ -214,7 +214,7 @@ [] => (Binding.name x, NoSyn) | [((b, _), mx)] => let - val y = Name.of_binding b; + val y = Variable.name b; val _ = x = y orelse error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.str_of (Binding.pos_of b)); @@ -253,7 +253,7 @@ [] => (Binding.name x, NoSyn) | [((b, _), mx)] => let - val y = Name.of_binding b; + val y = Variable.name b; val _ = x = y orelse error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.str_of (Binding.pos_of b)); @@ -323,10 +323,10 @@ | Element.Obtains obtains => let val case_names = obtains |> map_index (fn (i, (b, _)) => - if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b); + if Binding.is_empty b then string_of_int (i + 1) else Variable.name b); val constraints = obtains |> map (fn (_, (vars, _)) => Element.Constrains - (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE))); + (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE))); val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt; @@ -336,7 +336,7 @@ fun assume_case ((name, (vars, _)), asms) ctxt' = let val bs = map fst vars; - val xs = map Name.of_binding bs; + val xs = map Variable.name bs; val props = map fst asms; val (Ts, _) = ctxt' |> fold Variable.declare_term props diff -r e8777e3ea6ef -r 3305f573294e src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/ROOT.ML Sat Apr 16 12:46:18 2011 +0200 @@ -46,7 +46,6 @@ use "General/linear_set.ML"; use "General/long_name.ML"; use "General/binding.ML"; -use "General/name_space.ML"; use "General/path.ML"; use "General/url.ML"; use "General/buffer.ML"; @@ -111,6 +110,7 @@ use "context.ML"; use "config.ML"; use "context_position.ML"; +use "General/name_space.ML"; use "sorts.ML"; use "type.ML"; use "logic.ML"; diff -r e8777e3ea6ef -r 3305f573294e src/Pure/name.ML --- a/src/Pure/name.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/name.ML Sat Apr 16 12:46:18 2011 +0200 @@ -8,7 +8,6 @@ sig val uu: string val aT: string - val of_binding: binding -> string val bound: int -> string val is_bound: string -> bool val internal: string -> string @@ -43,11 +42,6 @@ (** special variable names **) -(* checked binding *) - -val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming; - - (* encoded bounds *) (*names for numbered variables -- diff -r e8777e3ea6ef -r 3305f573294e src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Apr 15 15:33:57 2011 +0200 +++ b/src/Pure/variable.ML Sat Apr 16 12:46:18 2011 +0200 @@ -19,6 +19,7 @@ val is_fixed: Proof.context -> string -> bool val newly_fixed: Proof.context -> Proof.context -> string -> bool val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list + val name: binding -> string val default_type: Proof.context -> string -> typ option val def_type: Proof.context -> bool -> indexname -> typ option val def_sort: Proof.context -> indexname -> sort option @@ -155,6 +156,9 @@ fun add_fixed ctxt = Term.fold_aterms (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I); +(*checked name binding*) +val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming; + (** declarations **)