--- a/src/Cube/Cube.thy Sun Feb 21 21:08:25 2010 +0100
+++ b/src/Cube/Cube.thy Sun Feb 21 21:10:01 2010 +0100
@@ -18,43 +18,43 @@
context' typing'
consts
- Abs :: "[term, term => term] => term"
- Prod :: "[term, term => term] => term"
- Trueprop :: "[context, typing] => prop"
- MT_context :: "context"
- Context :: "[typing, context] => context"
- star :: "term" ("*")
- box :: "term" ("[]")
- app :: "[term, term] => term" (infixl "^" 20)
- Has_type :: "[term, term] => typing"
+ Abs :: "[term, term => term] => term"
+ Prod :: "[term, term => term] => term"
+ Trueprop :: "[context, typing] => prop"
+ MT_context :: "context"
+ Context :: "[typing, context] => context"
+ star :: "term" ("*")
+ box :: "term" ("[]")
+ app :: "[term, term] => term" (infixl "^" 20)
+ Has_type :: "[term, term] => typing"
syntax
- Trueprop :: "[context', typing'] => prop" ("(_/ |- _)")
- Trueprop1 :: "typing' => prop" ("(_)")
- "" :: "id => context'" ("_")
- "" :: "var => context'" ("_")
- MT_context :: "context'" ("")
- Context :: "[typing', context'] => context'" ("_ _")
- Has_type :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5)
- Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
- arrow :: "[term, term] => term" (infixr "->" 10)
+ "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ |- _)")
+ "_Trueprop1" :: "typing' => prop" ("(_)")
+ "" :: "id => context'" ("_")
+ "" :: "var => context'" ("_")
+ "\<^const>Cube.MT_context" :: "context'" ("")
+ "\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _")
+ "\<^const>Cube.Has_type" :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5)
+ "_Lam" :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
+ "_Pi" :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
+ "_arrow" :: "[term, term] => term" (infixr "->" 10)
translations
("prop") "x:X" == ("prop") "|- x:X"
- "Lam x:A. B" == "CONST Abs(A, %x. B)"
- "Pi x:A. B" => "CONST Prod(A, %x. B)"
- "A -> B" => "CONST Prod(A, %_. B)"
+ "Lam x:A. B" == "CONST Abs(A, %x. B)"
+ "Pi x:A. B" => "CONST Prod(A, %x. B)"
+ "A -> B" => "CONST Prod(A, %_. B)"
syntax (xsymbols)
- Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
- box :: "term" ("\<box>")
- Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
- arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)
+ "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
+ "\<^const>Cube.box" :: "term" ("\<box>")
+ "_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
+ "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
+ "_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10)
print_translation {*
- [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))]
+ [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
*}
axioms
--- a/src/HOL/List.thy Sun Feb 21 21:08:25 2010 +0100
+++ b/src/HOL/List.thy Sun Feb 21 21:10:01 2010 +0100
@@ -358,11 +358,11 @@
parse_translation (advanced) {*
let
- val NilC = Syntax.const @{const_name Nil};
- val ConsC = Syntax.const @{const_name Cons};
- val mapC = Syntax.const @{const_name map};
- val concatC = Syntax.const @{const_name concat};
- val IfC = Syntax.const @{const_name If};
+ val NilC = Syntax.const @{const_syntax Nil};
+ val ConsC = Syntax.const @{const_syntax Cons};
+ val mapC = Syntax.const @{const_syntax map};
+ val concatC = Syntax.const @{const_syntax concat};
+ val IfC = Syntax.const @{const_syntax If};
fun singl x = ConsC $ x $ NilC;
@@ -371,12 +371,14 @@
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
val e = if opti then singl e else e;
val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
- val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const Term.dummy_patternN $ NilC;
+ val case2 =
+ Syntax.const @{syntax_const "_case1"} $
+ Syntax.const @{const_syntax dummy_pattern} $ NilC;
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
in lambda x ft end;
- fun abs_tr ctxt (p as Free(s,T)) e opti =
+ fun abs_tr ctxt (p as Free (s, T)) e opti =
let
val thy = ProofContext.theory_of ctxt;
val s' = Sign.intern_const thy s;
--- a/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 21:08:25 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 21:10:01 2010 +0100
@@ -310,6 +310,8 @@
fun case_tr err tab_of ctxt [t, u] =
let
val thy = ProofContext.theory_of ctxt;
+ val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy);
+
(* replace occurrences of dummy_pattern by distinct variables *)
(* internalize constant names *)
fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
@@ -319,9 +321,7 @@
let val x = Name.variant used "x"
in (Free (x, T), x :: used) end
| prep_pat (Const (s, T)) used =
- (case try (unprefix Syntax.constN) s of
- SOME c => (Const (c, T), used)
- | NONE => (Const (Sign.intern_const thy s, T), used))
+ (Const (intern_const_syntax s, T), used)
| prep_pat (v as Free (s, T)) used =
let val s' = Sign.intern_const thy s
in
@@ -455,14 +455,13 @@
fun case_tr' tab_of cname ctxt ts =
let
val thy = ProofContext.theory_of ctxt;
- val consts = ProofContext.consts_of ctxt;
fun mk_clause (pat, rhs) =
let val xs = Term.add_frees pat []
in
Syntax.const @{syntax_const "_case1"} $
map_aterms
(fn Free p => Syntax.mark_boundT p
- | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
+ | Const (s, _) => Syntax.const (Syntax.constN ^ s)
| t => t) pat $
map_aterms
(fn x as Free (s, T) =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:08:25 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:10:01 2010 +0100
@@ -223,7 +223,7 @@
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
- let val case_name' = Sign.const_syntax_name thy case_name
+ let val case_name' = Syntax.constN ^ case_name
in (case_name', Datatype_Case.case_tr' info_of_case case_name')
end) case_names, []) thy;
--- a/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:08:25 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:10:01 2010 +0100
@@ -15,15 +15,14 @@
(* nibble *)
-val nib_prefix = "String.nibble.";
-
val mk_nib =
- Syntax.Constant o unprefix nib_prefix o
+ Syntax.Constant o prefix Syntax.constN o
fst o Term.dest_Const o HOLogic.mk_nibble;
-fun dest_nib (Syntax.Constant c) =
- HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
- handle TERM _ => raise Match;
+fun dest_nib (Syntax.Constant s) =
+ (case try (unprefix Syntax.constN) s of
+ NONE => raise Match
+ | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
(* char *)