# HG changeset patch # User wenzelm # Date 1395398552 -3600 # Node ID 029246729dc09baa0afedcb7d2a8b538a172e766 # Parent 938c6c7e10ebb29b8e59e26960a8975cde942045 more qualified names; diff -r 938c6c7e10eb -r 029246729dc0 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Fri Mar 21 11:06:39 2014 +0100 +++ b/src/HOL/Code_Evaluation.thy Fri Mar 21 11:42:32 2014 +0100 @@ -85,8 +85,9 @@ begin definition - "term_of (f \ 'a \ 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') - [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" + "term_of (f \ 'a \ 'b) = + Const (STR ''Pure.dummy_pattern'') + (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" instance .. diff -r 938c6c7e10eb -r 029246729dc0 src/HOL/List.thy --- a/src/HOL/List.thy Fri Mar 21 11:06:39 2014 +0100 +++ b/src/HOL/List.thy Fri Mar 21 11:42:32 2014 +0100 @@ -439,7 +439,7 @@ val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; val case2 = Syntax.const @{syntax_const "_case1"} $ - Syntax.const @{const_syntax dummy_pattern} $ NilC; + Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC; val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end; diff -r 938c6c7e10eb -r 029246729dc0 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 11:42:32 2014 +0100 @@ -218,7 +218,7 @@ (@{const_name induct_conj}, "'a"),*) (@{const_name "undefined"}, "'a"), (@{const_name "default"}, "'a"), - (@{const_name "dummy_pattern"}, "'a::{}"), + (@{const_name "Pure.dummy_pattern"}, "'a::{}"), (@{const_name "HOL.simp_implies"}, "prop => prop => prop"), (@{const_name "bot_fun_inst.bot_fun"}, "'a"), (@{const_name "top_fun_inst.top_fun"}, "'a"), @@ -254,7 +254,7 @@ "HOL.induct_forall", @{const_name undefined}, @{const_name default}, - @{const_name dummy_pattern}, + @{const_name Pure.dummy_pattern}, @{const_name "HOL.simp_implies"}, @{const_name "bot_fun_inst.bot_fun"}, @{const_name "top_fun_inst.top_fun"}, diff -r 938c6c7e10eb -r 029246729dc0 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Mar 21 11:42:32 2014 +0100 @@ -149,7 +149,7 @@ | abs_pat _ _ = I; (* replace occurrences of dummy_pattern by distinct variables *) - fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used = + fun replace_dummies (Const (@{const_syntax Pure.dummy_pattern}, T)) used = let val (x, used') = variant_free "x" used in (Free (x, T), used') end | replace_dummies (t $ u) used = diff -r 938c6c7e10eb -r 029246729dc0 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 21 11:42:32 2014 +0100 @@ -428,7 +428,7 @@ fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = let val frees = Term.add_free_names t [] - val dummy_term = @{term "Code_Evaluation.Const (STR ''dummy_pattern'') + val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"} val return = @{term "Some :: term list => term list option"} $ (HOLogic.mk_list @{typ "term"} diff -r 938c6c7e10eb -r 029246729dc0 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 11:42:32 2014 +0100 @@ -127,8 +127,8 @@ Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf)) | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = AbsP (s, case t of - Const ("dummy_pattern", _) => NONE - | _ $ Const ("dummy_pattern", _) => NONE + Const ("Pure.dummy_pattern", _) => NONE + | _ $ Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t), Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = @@ -136,7 +136,7 @@ | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = prf_of (T::Ts) prf | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % - (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t)) + (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) | prf_of _ t = error ("Not a proof term:\n" ^ Syntax.string_of_term_global thy t) diff -r 938c6c7e10eb -r 029246729dc0 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Mar 21 11:42:32 2014 +0100 @@ -177,7 +177,7 @@ in [Ast.Constant (Lexicon.mark_type c)] end | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok - | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) = + | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) = [ast_of_dummy a tok] | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) = [ast_of_dummy a tok] diff -r 938c6c7e10eb -r 029246729dc0 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/Pure/pure_thy.ML Fri Mar 21 11:42:32 2014 +0100 @@ -170,7 +170,7 @@ ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"), ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"), (const "==>", typ "prop => prop => prop", Delimfix "op ==>"), - (const "dummy_pattern", typ "aprop", Delimfix "'_"), + (const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"), ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] @@ -200,12 +200,12 @@ (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), (Binding.name "prop", typ "prop => prop", NoSyn), (Binding.name "TYPE", typ "'a itself", NoSyn), - (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")] + (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")] #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") [] #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") [] #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") [] #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") [] - #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") [] + #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") [] #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation #> Sign.parse_translation Syntax_Trans.pure_parse_translation #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation diff -r 938c6c7e10eb -r 029246729dc0 src/Pure/term.ML --- a/src/Pure/term.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/Pure/term.ML Fri Mar 21 11:42:32 2014 +0100 @@ -924,18 +924,18 @@ (* dummy patterns *) -fun dummy_pattern T = Const ("dummy_pattern", T); +fun dummy_pattern T = Const ("Pure.dummy_pattern", T); val dummy = dummy_pattern dummyT; val dummy_prop = dummy_pattern propT; -fun is_dummy_pattern (Const ("dummy_pattern", _)) = true +fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true | is_dummy_pattern _ = false; fun no_dummy_patterns tm = if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); -fun free_dummy_patterns (Const ("dummy_pattern", T)) used = +fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used = let val [x] = Name.invent used Name.uu 1 in (Free (Name.internal x, T), Name.declare x used) end | free_dummy_patterns (Abs (x, T, b)) used = @@ -948,7 +948,7 @@ in (t' $ u', used'') end | free_dummy_patterns a used = (a, used); -fun replace_dummy Ts (Const ("dummy_pattern", T)) i = +fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i = (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_dummy Ts (Abs (x, T, t)) i = let val (t', i') = replace_dummy (T :: Ts) t i diff -r 938c6c7e10eb -r 029246729dc0 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Mar 21 11:06:39 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Fri Mar 21 11:42:32 2014 +0100 @@ -800,8 +800,8 @@ val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; - val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t; - val dummy_constant = Constant @{const_name dummy_pattern}; + val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t; + val dummy_constant = Constant @{const_name Pure.dummy_pattern}; val stmt_value = fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs ##>> translate_typ ctxt algbr eqngr false ty @@ -818,7 +818,7 @@ val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; in ((program3, ((vs_ty, t), deps')), (deps, program2)) end; in - ensure_stmt Constant stmt_value @{const_name dummy_pattern} + ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern} #> snd #> term_value end;