--- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 23:30:18 2011 +0200
@@ -854,8 +854,8 @@
@{index_ML_type Name.context} \\
@{index_ML Name.context: Name.context} \\
@{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
- @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
- @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
+ @{index_ML Name.invent: "Name.context -> string -> int -> string list"} \\
+ @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML Variable.names_of: "Proof.context -> Name.context"} \\
@@ -875,11 +875,11 @@
\item @{ML Name.declare}~@{text "name"} enters a used name into the
context.
- \item @{ML Name.invents}~@{text "context name n"} produces @{text
+ \item @{ML Name.invent}~@{text "context name n"} produces @{text
"n"} fresh names derived from @{text "name"}.
- \item @{ML Name.variants}~@{text "names context"} produces fresh
- variants of @{text "names"}; the result is entered into the context.
+ \item @{ML Name.variant}~@{text "name context"} produces a fresh
+ variant of @{text "name"}; the result is declared to the context.
\item @{ML Variable.names_of}~@{text "ctxt"} retrieves the context
of declared type and term variable names. Projecting a proof
@@ -897,11 +897,11 @@
fresh names from the initial @{ML Name.context}. *}
ML {*
- val list1 = Name.invents Name.context "a" 5;
+ val list1 = Name.invent Name.context "a" 5;
@{assert} (list1 = ["a", "b", "c", "d", "e"]);
val list2 =
- #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
+ #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context);
@{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
*}
@@ -914,11 +914,11 @@
ML {*
val names = Variable.names_of @{context};
- val list1 = Name.invents names "a" 5;
+ val list1 = Name.invent names "a" 5;
@{assert} (list1 = ["d", "e", "f", "g", "h"]);
val list2 =
- #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
+ #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] names);
@{assert} (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]);
*}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 15:14:21 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 23:30:18 2011 +0200
@@ -1254,8 +1254,8 @@
\indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
\indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
\indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
- \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
- \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
+ \indexdef{}{ML}{Name.invent}\verb|Name.invent: Name.context -> string -> int -> string list| \\
+ \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\
@@ -1275,10 +1275,10 @@
\item \verb|Name.declare|~\isa{name} enters a used name into the
context.
- \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
+ \item \verb|Name.invent|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
- \item \verb|Name.variants|~\isa{names\ context} produces fresh
- variants of \isa{names}; the result is entered into the context.
+ \item \verb|Name.variant|~\isa{name\ context} produces a fresh
+ variant of \isa{name}; the result is declared to the context.
\item \verb|Variable.names_of|~\isa{ctxt} retrieves the context
of declared type and term variable names. Projecting a proof
@@ -1325,7 +1325,7 @@
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ Name{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invent\ Name{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
@@ -1333,7 +1333,7 @@
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}b{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
@@ -1370,7 +1370,7 @@
\endisaantiq
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ names\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invent\ names\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
@@ -1378,7 +1378,7 @@
\ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}g{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}h{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
--- a/doc-src/IsarRef/Thy/Generic.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Thu Jun 09 23:30:18 2011 +0200
@@ -961,7 +961,11 @@
ones it cannot prove. Occasionally, attempting to prove the hard
ones may take a long time.
- %FIXME auto nat arguments
+ The optional depth arguments in @{text "(auto m n)"} refer to its
+ builtin classical reasoning procedures: @{text m} (default 4) is for
+ @{method blast}, which is tried first, and @{text n} (default 2) is
+ for a slower but more general alternative that also takes wrappers
+ into account.
\item @{method force} is intended to prove the first subgoal
completely, using many fancy proof tools and performing a rather
--- a/doc-src/IsarRef/Thy/document/Generic.tex Thu Jun 09 15:14:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Thu Jun 09 23:30:18 2011 +0200
@@ -1513,7 +1513,11 @@
ones it cannot prove. Occasionally, attempting to prove the hard
ones may take a long time.
- %FIXME auto nat arguments
+ The optional depth arguments in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}auto\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} refer to its
+ builtin classical reasoning procedures: \isa{m} (default 4) is for
+ \hyperlink{method.blast}{\mbox{\isa{blast}}}, which is tried first, and \isa{n} (default 2) is
+ for a slower but more general alternative that also takes wrappers
+ into account.
\item \hyperlink{method.force}{\mbox{\isa{force}}} is intended to prove the first subgoal
completely, using many fancy proof tools and performing a rather
--- a/lib/texinputs/isabelle.sty Thu Jun 09 15:14:21 2011 +0200
+++ b/lib/texinputs/isabelle.sty Thu Jun 09 23:30:18 2011 +0200
@@ -15,17 +15,26 @@
\newcommand{\isastyletxt}{\rm}
\newcommand{\isastylecmt}{\rm}
+\newcommand{\isaspacing}{%
+ \sfcode 42 1000 % .
+ \sfcode 63 1000 % ?
+ \sfcode 33 1000 % !
+ \sfcode 58 1000 % :
+ \sfcode 59 1000 % ;
+ \sfcode 44 1000 % ,
+}
+
%symbol markup -- \emph achieves decent spacing via italic corrections
\newcommand{\isamath}[1]{\emph{$#1$}}
\newcommand{\isatext}[1]{\emph{#1}}
-\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
-\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
@@ -40,13 +49,13 @@
\isamarkuptrue\par%
\isa@parindent\parindent\parindent0pt%
\isa@parskip\parskip\parskip0pt%
-\isastyle}{\par}
+\isaspacing\isastyle}{\par}
\newenvironment{isabelle}
{\begin{trivlist}\begin{isabellebody}\item\relax}
{\end{isabellebody}\end{trivlist}}
-\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
+\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
\newcommand{\isaindent}[1]{\hphantom{#1}}
\newcommand{\isanewline}{\mbox{}\par\mbox{}}
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 23:30:18 2011 +0200
@@ -86,7 +86,7 @@
SOME type_name => (((name, type_name), log_ex name type_name), thy)
| NONE =>
let
- val args = map (rpair dummyS) (Name.invents Name.context "'a" arity)
+ val args = map (rpair dummyS) (Name.invent Name.context "'a" arity)
val (T, thy') =
Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
val type_name = fst (Term.dest_Type T)
@@ -446,8 +446,7 @@
val nctxt = Name.make_context (duplicates (op =) (names_of t []))
fun fresh (i, nctxt) = (position_prefix ^ string_of_int i, (i+1, nctxt))
- fun renamed n (i, nctxt) =
- yield_singleton Name.variants n nctxt ||> pair i
+ fun renamed n (i, nctxt) = Name.variant n nctxt ||> pair i
fun mk_label (name, t) = @{term assert_at} $ Free (name, @{typ bool}) $ t
fun unique t =
@@ -472,11 +471,11 @@
all_names
|> map_filter (try (fn n => (n, short_var_name n)))
|> split_list
- ||>> (fn names => Name.variants names (Name.make_context all_names))
+ ||>> (fn names => fold_map Name.variant names (Name.make_context all_names))
|>> Symtab.make o (op ~~)
fun rename_free n = the_default n (Symtab.lookup names n)
- fun rename_abs n = yield_singleton Name.variants (short_var_name n)
+ fun rename_abs n = Name.variant (short_var_name n)
fun rename _ (Free (n, T)) = Free (rename_free n, T)
| rename nctxt (Abs (n, T, t)) =
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Jun 09 23:30:18 2011 +0200
@@ -67,8 +67,8 @@
fun fw mi th th' th'' =
let
val th0 = if mi then
- instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
- else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
+ Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
+ else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
@@ -114,11 +114,11 @@
val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
- nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
+ nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
- npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
+ npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
- ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
+ ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
fun decomp_mpinf fm =
case term_of fm of
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jun 09 23:30:18 2011 +0200
@@ -403,7 +403,7 @@
(* calculate function arguments of case combinator *)
val tns = map fst (Term.add_tfreesT lhsT [])
- val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
+ val resultT = TFree (singleton (Name.variant_list tns) "'t", @{sort pcpo})
fun fTs T = map (fn (_, args) => map snd args -->> T) spec
val fns = Datatype_Prop.indexify_names (map (K "f") spec)
val fs = map Free (fns ~~ fTs resultT)
@@ -768,7 +768,7 @@
val resultT : typ =
let
val ts : string list = map fst (Term.add_tfreesT lhsT [])
- val t : string = Name.variant ts "'t"
+ val t : string = singleton (Name.variant_list ts) "'t"
in TFree (t, @{sort pcpo}) end
(* define match combinators *)
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Thu Jun 09 23:30:18 2011 +0200
@@ -23,7 +23,7 @@
fun trans_rules name2 name1 n mx =
let
- val vnames = Name.invents Name.context "a" n
+ val vnames = Name.invent Name.context "a" n
val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
in
[Syntax.Parse_Print_Rule
--- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 09 23:30:18 2011 +0200
@@ -234,7 +234,7 @@
in comp_con T f rhs' (v::vs) taken' end
| Const (c, cT) =>
let
- val n = Name.variant taken "v"
+ val n = singleton (Name.variant_list taken) "v"
val v = Free(n, T)
val m = Const(match_name c, matcherT (cT, fastype_of rhs))
val k = big_lambdas vs rhs
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Jun 09 23:30:18 2011 +0200
@@ -531,7 +531,7 @@
(* prove strictness and reduction rules of pattern combinators *)
local
val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
- val rn = Name.variant tns "'r";
+ val rn = singleton (Name.variant_list tns) "'r";
val R = TFree (rn, @{sort pcpo});
fun pat_lhs (pat, args) =
let
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 23:30:18 2011 +0200
@@ -618,7 +618,6 @@
open Code_Thingol;
fun imp_program naming =
-
let
fun is_const c = case lookup_const naming c
of SOME c' => (fn c'' => c' = c'')
@@ -635,7 +634,7 @@
| dest_abs (t, ty) =
let
val vs = fold_varnames cons t [];
- val v = Name.variant vs "x";
+ val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
fun force (t as IConst (c, _) `$ t') = if is_return c
--- a/src/HOL/Import/hol4rews.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML Thu Jun 09 23:30:18 2011 +0200
@@ -605,7 +605,7 @@
then F defname (* name_def *)
else if not (member (op =) used pdefname)
then F pdefname (* name_primdef *)
- else F (Name.variant used pdefname) (* last resort *)
+ else F (singleton (Name.variant_list used) pdefname) (* last resort *)
end
end
--- a/src/HOL/Import/proof_kernel.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu Jun 09 23:30:18 2011 +0200
@@ -1419,7 +1419,7 @@
| NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
))
(zip tys_before tys_after)
- val res = Drule.instantiate (tyinst,[]) th1
+ val res = Drule.instantiate_normalize (tyinst,[]) th1
val hth = HOLThm([],res)
val res = norm_hthm thy hth
val _ = message "RESULT:"
--- a/src/HOL/Import/shuffler.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Import/shuffler.ML Thu Jun 09 23:30:18 2011 +0200
@@ -228,7 +228,7 @@
val (type_inst,_) =
fold (fn (w as (v,_), S) => fn (inst, used) =>
let
- val v' = Name.variant used v
+ val v' = singleton (Name.variant_list used) v
in
((w,TFree(v',S))::inst,v'::used)
end)
@@ -249,7 +249,7 @@
val mid =
case rens of
[] => thm'
- | [((_, S), idx)] => instantiate
+ | [((_, S), idx)] => Drule.instantiate_normalize
([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
| _ => error "Shuffler.inst_tfrees internal error"
in
@@ -298,7 +298,7 @@
then
let
val cert = cterm_of thy
- val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
+ val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT)
val cv = cert v
val ct = cert t
val th = (Thm.assume ct)
@@ -361,7 +361,7 @@
Type("fun",[aT,bT]) =>
let
val cert = cterm_of thy
- val vname = Name.variant (Term.add_free_names t []) "v"
+ val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
val v = Free(vname,aT)
val cv = cert v
val ct = cert t
--- a/src/HOL/Inductive.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Inductive.thy Thu Jun 09 23:30:18 2011 +0200
@@ -295,7 +295,8 @@
let
fun fun_tr ctxt [cs] =
let
- val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
+ (* FIXME proper name context!? *)
+ val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
in lambda x ft end
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
--- a/src/HOL/Library/Efficient_Nat.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Jun 09 23:30:18 2011 +0200
@@ -113,8 +113,8 @@
fun remove_suc thy thms =
let
- val vname = Name.variant (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
+ val vname = singleton (Name.variant_list (map fst
+ (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
fun lhs_of th = snd (Thm.dest_comb
(fst (Thm.dest_comb (cprop_of th))));
@@ -166,8 +166,8 @@
fun remove_suc_clause thy thms =
let
- val vname = Name.variant (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
+ val vname = singleton (Name.variant_list (map fst
+ (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
| find_var _ = NONE;
--- a/src/HOL/Library/reflection.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Library/reflection.ML Thu Jun 09 23:30:18 2011 +0200
@@ -157,7 +157,7 @@
map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
in ((fts ~~ (replicate (length fts) ctxt),
- Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
+ Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
end;
@@ -230,7 +230,7 @@
val substt =
let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end
- val th = (instantiate (subst_ty, substt) eq) RS sym
+ val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym
in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
handle Pattern.MATCH => tryeqs eqs bds)
in tryeqs (filter isat eqs) bds end), bds);
@@ -277,7 +277,7 @@
val cert = cterm_of (Proof_Context.theory_of ctxt)
val cvs = map (fn (v as Var(n,t)) => (cert v,
the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
- val th' = instantiate ([], cvs) th
+ val th' = Drule.instantiate_normalize ([], cvs) th
val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
(fn _ => simp_tac (simpset_of ctxt) 1)
--- a/src/HOL/List.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/List.thy Thu Jun 09 23:30:18 2011 +0200
@@ -383,7 +383,8 @@
fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
let
- val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
+ (* FIXME proper name context!? *)
+ val x = Free (singleton (Name.variant_list (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"} $ Term_Position.strip_positions p $ e;
val case2 =
--- a/src/HOL/Multivariate_Analysis/normarith.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Thu Jun 09 23:30:18 2011 +0200
@@ -306,7 +306,7 @@
(fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
in fst (RealArith.real_linear_prover translator
- (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
+ (map (fn t => Drule.instantiate_normalize ([(tv_n, ctyp_of_term t)],[]) pth_zero)
zerodests,
map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
@@ -343,7 +343,7 @@
val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
val cps = map (swap o Thm.dest_equals) (cprems_of th11)
- val th12 = instantiate ([], cps) th11
+ val th12 = Drule.instantiate_normalize ([], cps) th11
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
in hd (Variable.export ctxt' ctxt [th13])
end
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 09 23:30:18 2011 +0200
@@ -622,7 +622,7 @@
(resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
let
val permT = mk_permT
- (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
+ (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
val pi = Free ("pi", permT);
val T = Type (Sign.intern_type thy name, map TFree tvs);
in apfst (pair r o hd)
@@ -1169,7 +1169,7 @@
val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val frees' = partition_cargs idxs frees;
- val z = (Name.variant tnames "z", fsT);
+ val z = (singleton (Name.variant_list tnames) "z", fsT);
fun mk_prem ((dt, s), T) =
let
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Jun 09 23:30:18 2011 +0200
@@ -200,7 +200,7 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
- val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
+ val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 23:30:18 2011 +0200
@@ -226,7 +226,7 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Long_Name.base_name a)) atoms));
- val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
+ val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 23:30:18 2011 +0200
@@ -36,7 +36,7 @@
let
val (vs, Ts) = split_list (strip_qnt_vars "all" t);
val body = strip_qnt_body "all" t;
- val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
+ val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []))
in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
@@ -207,7 +207,7 @@
fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
let
val used = map fst (fold Term.add_frees fs []);
- val x = (Name.variant used "x", dummyT);
+ val x = (singleton (Name.variant_list used) "x", dummyT);
val frees = ls @ x :: rs;
val raw_rhs = list_abs_free (frees,
list_comb (Const (rec_name, dummyT), fs @ [Free x]))
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 09 23:30:18 2011 +0200
@@ -136,7 +136,7 @@
fun mk_variables thy prfx xs ty (tab, ctxt) =
let
val T = mk_type thy prfx ty;
- val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
+ val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
val zs = map (Free o rpair T) ys;
in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
@@ -779,7 +779,7 @@
map_filter (fn s => lookup funs s |>
Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
split_list ||> split_list;
- val (fs', ctxt') = Name.variants fs ctxt
+ val (fs', ctxt') = fold_map Name.variant fs ctxt
in
(fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
Element.Fixes (map2 (fn s => fn T =>
--- a/src/HOL/Statespace/state_space.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Jun 09 23:30:18 2011 +0200
@@ -379,8 +379,8 @@
val Ts = distinct_types (map snd all_comps);
val arg_names = map fst args;
- val valueN = Name.variant arg_names "'value";
- val nameN = Name.variant (valueN::arg_names) "'name";
+ val valueN = singleton (Name.variant_list arg_names) "'value";
+ val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
val valueT = TFree (valueN, Sign.defaultS thy);
val nameT = TFree (nameN, Sign.defaultS thy);
val stateT = nameT --> valueT;
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 23:30:18 2011 +0200
@@ -849,7 +849,7 @@
|>> (introduce_proxies format type_sys #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q s T t' =
- let val s = Name.variant (map fst bs) s in
+ let val s = singleton (Name.variant_list (map fst bs)) s in
do_formula ((s, T) :: bs) t'
#>> mk_aquant q [(`make_bound_var s, SOME T)]
end
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jun 09 23:30:18 2011 +0200
@@ -281,7 +281,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (Name.variant used "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
--- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Jun 09 23:30:18 2011 +0200
@@ -152,7 +152,7 @@
fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
let
- val name = Name.variant used "a";
+ val name = singleton (Name.variant_list used) "a";
fun expand constructors used ty ((_, []), _) =
raise CASE_ERROR ("mk_case: expand_var_row", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
@@ -264,11 +264,12 @@
(* replace occurrences of dummy_pattern by distinct variables *)
(* internalize constant names *)
+ (* FIXME proper name context!? *)
fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
let val (t', used') = prep_pat t used
in (c $ t' $ tT, used') end
| prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
- let val x = Name.variant used "x"
+ let val x = singleton (Name.variant_list used) "x"
in (Free (x, T), x :: used) end
| prep_pat (Const (s, T)) used =
(Const (intern_const_syntax s, T), used)
@@ -305,6 +306,7 @@
(* destruct one level of pattern matching *)
+(* FIXME proper name context!? *)
fun gen_dest_case name_of type_of tab d used t =
(case apfst name_of (strip_comb t) of
(SOME cname, ts as _ :: _) =>
@@ -345,7 +347,7 @@
val R = type_of t;
val dummy =
if d then Const (@{const_name dummy_pattern}, R)
- else Free (Name.variant used "x", R);
+ else Free (singleton (Name.variant_list used) "x", R);
in
SOME (x,
map mk_case
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Jun 09 23:30:18 2011 +0200
@@ -47,7 +47,7 @@
|> Term.strip_comb
|> apsnd (fst o split_last)
|> list_comb;
- val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
+ val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
in
thms
--- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 23:30:18 2011 +0200
@@ -134,7 +134,7 @@
val names = map Long_Name.base_name (the_default tycos (#alt_names info));
val (auxnames, _) = Name.make_context names
- |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
+ |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
val prefix = space_implode "_" names;
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
@@ -407,7 +407,7 @@
fun inter_sort m = map (fn xs => nth xs m) raw_vss
|> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
val sorts = map inter_sort ms;
- val vs = Name.names Name.context Name.aT sorts;
+ val vs = Name.invent_names Name.context Name.aT sorts;
fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
(TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Jun 09 23:30:18 2011 +0200
@@ -263,7 +263,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (Name.variant used "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -310,7 +310,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
--- a/src/HOL/Tools/Function/fun.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML Thu Jun 09 23:30:18 2011 +0200
@@ -64,7 +64,7 @@
val (argTs, rT) = chop n (binder_types fT)
|> apsnd (fn Ts => Ts ---> body_type fT)
- val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
+ val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
in
HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
Const ("HOL.undefined", rT))
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Jun 09 23:30:18 2011 +0200
@@ -75,7 +75,7 @@
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
(*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
| dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Jun 09 23:30:18 2011 +0200
@@ -167,12 +167,19 @@
(* INFERENCE RULE: RESOLVE *)
+(*Increment the indexes of only the type variables*)
+fun incr_type_indexes inc th =
+ let val tvs = Term.add_tvars (Thm.full_prop_of th) []
+ and thy = Thm.theory_of_thm th
+ fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
+ in Thm.instantiate (map inc_tvar tvs, []) th end;
+
(* Like RSN, but we rename apart only the type variables. Vars here typically
have an index of 1, and the use of RSN would increase this typically to 3.
Instantiations of those Vars could then fail. *)
fun resolve_inc_tyvars thy tha i thb =
let
- val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
fun aux tha thb =
case Thm.bicompose false (false, tha, nprems_of tha) i thb
|> Seq.list_of |> distinct Thm.eq_thm of
@@ -199,7 +206,7 @@
|> map (fn (x, (S, T)) =>
pairself (ctyp_of thy) (TVar (x, S), T)) of
[] => raise TERM z
- | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
+ | ps => aux (Drule.instantiate_normalize (ps, []) tha) (Drule.instantiate_normalize (ps, []) thb)
end
fun s_not (@{const Not} $ t) = t
@@ -555,7 +562,7 @@
tyenv []
val t_inst =
[pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
- in th |> instantiate (ty_inst, t_inst) end
+ in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
| _ => raise Fail "expected a single non-zapped, non-Metis Var"
in
(DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 23:30:18 2011 +0200
@@ -205,7 +205,7 @@
(filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
(Symbol.explode name)))
val name'' = f (if name' = "" then empty else name')
- in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+ in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
(** constant table **)
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 23:30:18 2011 +0200
@@ -249,7 +249,7 @@
end
else
let
- val s = Name.variant names "x"
+ val s = singleton (Name.variant_list names) "x"
val v = Free (s, fastype_of t)
in
(v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
@@ -257,7 +257,7 @@
(*
if is_constrt thy t then (t, (names, eqs)) else
let
- val s = Name.variant names "x"
+ val s = singleton (Name.variant_list names) "x"
val v = Free (s, fastype_of t)
in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
*)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 23:30:18 2011 +0200
@@ -542,7 +542,7 @@
fun focus_ex t nctxt =
let
val ((xs, Ts), t') = apfst split_list (strip_ex t)
- val (xs', nctxt') = Name.variants xs nctxt;
+ val (xs', nctxt') = fold_map Name.variant xs nctxt;
val ps' = xs' ~~ Ts;
val vs = map Free ps';
val t'' = Term.subst_bounds (rev vs, t');
@@ -906,7 +906,7 @@
val Type ("fun", [T, T']) = fastype_of comb;
val (Const (case_name, _), fs) = strip_comb comb
val used = Term.add_tfree_names comb []
- val U = TFree (Name.variant used "'t", HOLogic.typeS)
+ val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
val x = Free ("x", T)
val f = Free ("f", T' --> U)
fun apply_f f' =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 09 23:30:18 2011 +0200
@@ -302,7 +302,7 @@
mk_random = (fn _ => error "no random generation"),
additional_arguments = fn names =>
let
- val depth_name = Name.variant names "depth"
+ val depth_name = singleton (Name.variant_list names) "depth"
in [Free (depth_name, @{typ code_numeral})] end,
modify_funT = (fn T => let val (Ts, U) = strip_type T
val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
@@ -563,7 +563,7 @@
NONE => (Free (s, T), (names, (s, [])::vs))
| SOME xs =>
let
- val s' = Name.variant names s;
+ val s' = singleton (Name.variant_list names) s;
val v = Free (s', T)
in
(v, (s'::names, AList.update (op =) (s, v::xs) vs))
@@ -626,8 +626,8 @@
val eqs'' =
map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
- val name = Name.variant names "x";
- val name' = Name.variant (name :: names) "y";
+ val name = singleton (Name.variant_list names) "x";
+ val name' = singleton (Name.variant_list (name :: names)) "y";
val T = HOLogic.mk_tupleT (map fastype_of out_ts);
val U = fastype_of success_t;
val U' = dest_predT compfuns U;
@@ -905,7 +905,7 @@
let
val (i, is) = argument_position_of mode position
val inp_var = nth_pair is (nth in_ts' i)
- val x = Name.variant all_vs "x"
+ val x = singleton (Name.variant_list all_vs) "x"
val xt = Free (x, fastype_of inp_var)
fun compile_single_case ((c, T), switched) =
let
@@ -962,7 +962,7 @@
(Free (hd param_vs, T), (tl param_vs, names))
else
let
- val new = Name.variant names "x"
+ val new = singleton (Name.variant_list names) "x"
in (Free (new, T), (param_vs, new :: names)) end)) inpTs
(param_vs, (all_vs @ param_vs))
val in_ts' = map_filter (map_filter_prod
@@ -1009,7 +1009,7 @@
fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
if eq_mode (m, Input) orelse eq_mode (m, Output) then
let
- val x = Name.variant names "x"
+ val x = singleton (Name.variant_list names) "x"
in
(Free (x, T), x :: names)
end
@@ -1023,7 +1023,7 @@
| mk_args is_eval ((m as Fun _), T) names =
let
val funT = funT_of PredicateCompFuns.compfuns m T
- val x = Name.variant names "x"
+ val x = singleton (Name.variant_list names) "x"
val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
@@ -1033,7 +1033,7 @@
end
| mk_args is_eval (_, T) names =
let
- val x = Name.variant names "x"
+ val x = singleton (Name.variant_list names) "x"
in
(Free (x, T), x :: names)
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Jun 09 23:30:18 2011 +0200
@@ -129,7 +129,7 @@
fun declare_names s xs ctxt =
let
- val res = Name.names ctxt s xs
+ val res = Name.invent_names ctxt s xs
in (res, fold Name.declare (map fst res) ctxt) end
fun split_all_pairs thy th =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 23:30:18 2011 +0200
@@ -84,8 +84,8 @@
val (argTs, resT) = strip_type (fastype_of func)
val nctxt =
Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
- val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
- val ([resname], nctxt'') = Name.variants ["r"] nctxt'
+ val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
+ val (resname, nctxt'') = Name.variant "r" nctxt'
val args = map Free (argnames ~~ argTs)
val res = Free (resname, resT)
in Logic.mk_equals
@@ -118,7 +118,7 @@
val absnames = Name.variant_list names (map fst vars)
val frees = map2 (curry Free) absnames (map snd vars)
val body' = subst_bounds (rev frees, body)
- val resname = Name.variant (absnames @ names) "res"
+ val resname = singleton (Name.variant_list (absnames @ names)) "res"
val resvar = Free (resname, fastype_of body)
val t = flatten' body' ([], [])
|> map (fn (res, (inner_names, inner_prems)) =>
@@ -241,7 +241,7 @@
HOLogic.mk_eq (@{term False}, Bound 0)))
end
val argvs' = map2 lift_arg Ts argvs
- val resname = Name.variant names' "res"
+ val resname = singleton (Name.variant_list names') "res"
val resvar = Free (resname, body_type (fastype_of t))
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
in (resvar, (resname :: names', prem :: prems')) end))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Jun 09 23:30:18 2011 +0200
@@ -77,7 +77,7 @@
if is_compound atom then
let
val atom = Envir.beta_norm (Pattern.eta_long [] atom)
- val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val (params, args) = List.partition (is_predT o fastype_of)
@@ -108,7 +108,7 @@
| SOME (atom', srs) =>
let
val frees = map Free (Term.add_frees atom' [])
- val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val constT = map fastype_of frees ---> HOLogic.boolT
@@ -239,8 +239,9 @@
val vars = map Var (Term.add_vars abs_arg [])
val abs_arg' = Logic.unvarify_global abs_arg
val frees = map Free (Term.add_frees abs_arg' [])
- val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
- ((Long_Name.base_name constname) ^ "_hoaux")
+ val constname =
+ singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
+ ((Long_Name.base_name constname) ^ "_hoaux")
val full_constname = Sign.full_bname thy constname
val constT = map fastype_of frees ---> (fastype_of abs_arg')
val const = Const (full_constname, constT)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Jun 09 23:30:18 2011 +0200
@@ -73,7 +73,8 @@
fun mk_fresh_name names =
let
val name =
- Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+ singleton (Name.variant_list names)
+ ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
val bname = Sign.full_bname thy name
in
if Sign.declared_const thy bname then
@@ -119,7 +120,7 @@
val add_vars = fold_aterms (fn Var v => cons v | _ => I);
fun fresh_free T free_names =
let
- val free_name = Name.variant free_names "x"
+ val free_name = singleton (Name.variant_list free_names) "x"
in
(Free (free_name, T), free_name :: free_names)
end
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Jun 09 23:30:18 2011 +0200
@@ -156,10 +156,10 @@
[(th_1,th_2,th_3), (th_1',th_2',th_3')] =
let
val (mp', mq') = (get_pmi th_1, get_pmi th_1')
- val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
+ val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
[th_1, th_1']
- val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
- val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
+ val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
+ val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
in (mi_th, set_th, infD_th)
end;
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 23:30:18 2011 +0200
@@ -67,7 +67,7 @@
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
let
- val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
+ val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
$ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 09 23:30:18 2011 +0200
@@ -100,7 +100,7 @@
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;
val rule = @{thm random_aux_rec}
- |> Drule.instantiate ([(aT, icT)],
+ |> Drule.instantiate_normalize ([(aT, icT)],
[(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
val tac = ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac rew_ss)
@@ -214,7 +214,7 @@
val tTs = (map o apsnd) termifyT simple_tTs;
val is_rec = exists is_some ks;
val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
- val vs = Name.names Name.context "x" (map snd simple_tTs);
+ val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
val tc = HOLogic.mk_return T @{typ Random.seed}
(HOLogic.mk_valtermify_app c vs simpleT);
val t = HOLogic.mk_ST
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 09 23:30:18 2011 +0200
@@ -108,7 +108,7 @@
| SOME thm' =>
(case try (get_match_inst thy (get_lhs thm')) redex of
NONE => NONE
- | SOME inst2 => try (Drule.instantiate inst2) thm'))
+ | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
end
fun ball_bex_range_simproc ss redex =
@@ -490,7 +490,7 @@
if ty_c = ty_d
then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
- val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
+ val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
in
Conv.rewr_conv thm4 ctrm
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 23:30:18 2011 +0200
@@ -155,7 +155,7 @@
fun close_form t =
(t, [] |> Term.add_free_names t |> maps all_prefixes_of)
|> fold (fn ((s, i), T) => fn (t', taken) =>
- let val s' = Name.variant taken s in
+ let val s' = singleton (Name.variant_list taken) s in
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
else Term.all) T
$ Abs (s', T, abstract_over (Var ((s, i), T), t')),
--- a/src/HOL/Tools/TFL/rules.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Jun 09 23:30:18 2011 +0200
@@ -270,7 +270,7 @@
val gspec = Thm.forall_intr (cterm_of thy x) spec
in
fun SPEC tm thm =
- let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
+ let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_term tm)], []) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
@@ -298,7 +298,7 @@
val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
- val allI2 = instantiate (certify thy theta) allI
+ val allI2 = Drule.instantiate_normalize (certify thy theta) allI
val thm = Thm.implies_elim allI2 gth
val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
val prop' = tp $ (A $ Abs(x,ty,M))
--- a/src/HOL/Tools/TFL/tfl.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Jun 09 23:30:18 2011 +0200
@@ -324,7 +324,7 @@
map_index (fn (i, t) => (t,(i,true))) R)
val names = List.foldr OldTerm.add_term_names [] R
val atype = type_of(hd pats)
- and aname = Name.variant names "a"
+ and aname = singleton (Name.variant_list names) "a"
val a = Free(aname,atype)
val ty_info = Thry.match_info thy
val ty_match = Thry.match_type thy
@@ -480,7 +480,7 @@
val tych = Thry.typecheck thy
val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
+ val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
Rtype)
val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
@@ -679,8 +679,8 @@
in fn pats =>
let val names = List.foldr OldTerm.add_term_names [] pats
val T = type_of (hd pats)
- val aname = Name.variant names "a"
- val vname = Name.variant (aname::names) "v"
+ val aname = singleton (Name.variant_list names) "a"
+ val vname = singleton (Name.variant_list (aname::names)) "v"
val a = Free (aname, T)
val v = Free (vname, T)
val a_eq_v = HOLogic.mk_eq(a,v)
@@ -830,8 +830,8 @@
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
- val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
- [] (pats::TCsl)) "P"
+ val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
+ [] (pats::TCsl))) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = Rules.SPEC (tych P) Sinduction
val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
@@ -841,9 +841,10 @@
val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
val proved_cases = map (prove_case fconst thy) tasks
- val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
- "v",
- domain)
+ val v =
+ Free (singleton
+ (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
+ domain)
val vtyped = tych v
val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
--- a/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 23:30:18 2011 +0200
@@ -238,7 +238,7 @@
fun dest_abs used (a as Abs(s, ty, M)) =
let
- val s' = Name.variant used s;
+ val s' = singleton (Name.variant_list used) s;
val v = Free(s', ty);
in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
end
--- a/src/HOL/Tools/code_evaluation.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Thu Jun 09 23:30:18 2011 +0200
@@ -57,7 +57,7 @@
fun mk_term_of_eq thy ty (c, (_, tys)) =
let
val t = list_comb (Const (c, tys ---> ty),
- map Free (Name.names Name.context "a" tys));
+ map Free (Name.invent_names Name.context "a" tys));
val (arg, rhs) =
pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
(t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
--- a/src/HOL/Tools/enriched_type.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/enriched_type.ML Thu Jun 09 23:30:18 2011 +0200
@@ -98,7 +98,7 @@
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
fun invents n k nctxt =
let
- val names = Name.invents nctxt n k;
+ val names = Name.invent nctxt n k;
in (names, fold Name.declare names nctxt) end;
val ((names21, names32), nctxt) = Variable.names_of ctxt
|> invents "f" (length Ts21)
@@ -120,7 +120,7 @@
val mapper31 = mk_mapper T3 T1 args31;
val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(HOLogic.mk_comp (mapper21, mapper32), mapper31);
- val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
+ val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(mapper21 $ (mapper32 $ x), mapper31 $ x);
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 09 23:30:18 2011 +0200
@@ -326,7 +326,7 @@
(case AList.lookup (op =) vs s of
NONE => (s, (names, (s, [s])::vs))
| SOME xs =>
- let val s' = Name.variant names s
+ let val s' = singleton (Name.variant_list names) s
in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
fun distinct_v (Var ((s, 0), T)) nvs =
@@ -414,7 +414,7 @@
fun check_constrt t (names, eqs) =
if is_constrt thy t then (t, (names, eqs))
else
- let val s = Name.variant names "x";
+ let val s = singleton (Name.variant_list names) "x";
in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
fun compile_eq (s, t) gr =
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Jun 09 23:30:18 2011 +0200
@@ -36,7 +36,7 @@
fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
let val (s', names') = (case names of
- [] => (Name.variant used s, [])
+ [] => (singleton (Name.variant_list used) s, [])
| name :: names' => (name, names'))
in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
| strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
@@ -246,7 +246,7 @@
handle Datatype_Aux.Datatype_Empty name' =>
let
val name = Long_Name.base_name name';
- val dname = Name.variant used "Dummy";
+ val dname = singleton (Name.variant_list used) "Dummy";
in
thy
|> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
--- a/src/HOL/Tools/lin_arith.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Jun 09 23:30:18 2011 +0200
@@ -63,9 +63,9 @@
let
val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
and ct = cterm_of thy t
- in instantiate ([], [(cn, ct)]) @{thm le0} end;
+ in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
-end; (* LA_Logic *)
+end;
(* arith context data *)
--- a/src/HOL/Tools/primrec.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/primrec.ML Thu Jun 09 23:30:18 2011 +0200
@@ -38,7 +38,7 @@
let
val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
val body = strip_qnt_body "all" spec;
- val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
+ val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []));
val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)
--- a/src/HOL/Tools/record.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/record.ML Thu Jun 09 23:30:18 2011 +0200
@@ -1662,7 +1662,7 @@
val variants = map (fn Free (x, _) => x) vars_more;
val ext = mk_ext vars_more;
val s = Free (rN, extT);
- val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
+ val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
val inject_prop =
let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
@@ -1677,7 +1677,7 @@
(All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
val split_meta_prop =
- let val P = Free (Name.variant variants "P", extT --> Term.propT) in
+ let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
Logic.mk_equals
(All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
end;
@@ -1801,7 +1801,7 @@
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
val T = Type (tyco, map TFree vs);
val Tm = termifyT T;
- val params = Name.names Name.context "x" Ts;
+ val params = Name.invent_names Name.context "x" Ts;
val lhs = HOLogic.mk_random T size;
val tc = HOLogic.mk_return Tm @{typ Random.seed}
(HOLogic.mk_valtermify_app extN params T);
@@ -1820,7 +1820,7 @@
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
val T = Type (tyco, map TFree vs);
val test_function = Free ("f", termifyT T --> @{typ "term list option"});
- val params = Name.names Name.context "x" Ts;
+ val params = Name.invent_names Name.context "x" Ts;
fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
fun mk_full_exhaustive T =
@@ -1938,7 +1938,7 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
- val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
+ val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
@@ -2134,9 +2134,9 @@
(* prepare propositions *)
val _ = timing_msg "record preparing propositions";
- val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
- val C = Free (Name.variant all_variants "C", HOLogic.boolT);
- val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
+ val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
+ val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
+ val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
(*selectors*)
val sel_conv_props =
@@ -2145,7 +2145,8 @@
(*updates*)
fun mk_upd_prop i (c, T) =
let
- val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
+ val x' =
+ Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
val n = parent_fields_len + i;
val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
@@ -2174,7 +2175,9 @@
(*split*)
val split_meta_prop =
- let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
+ let
+ val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
+ in
Logic.mk_equals
(All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
end;
--- a/src/HOL/Tools/split_rule.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Tools/split_rule.ML Thu Jun 09 23:30:18 2011 +0200
@@ -73,7 +73,7 @@
val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
val (vs', insts) = fold mk_tuple ts (vs, []);
in
- (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+ (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
end
| complete_split_rule_var _ x = x;
--- a/src/HOL/Typerep.thy Thu Jun 09 15:14:21 2011 +0200
+++ b/src/HOL/Typerep.thy Thu Jun 09 23:30:18 2011 +0200
@@ -47,7 +47,7 @@
fun add_typerep tyco thy =
let
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
- val vs = Name.names Name.context "'a" sorts;
+ val vs = Name.invent_names Name.context "'a" sorts;
val ty = Type (tyco, map TFree vs);
val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
$ Free ("T", Term.itselfT ty);
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jun 09 23:30:18 2011 +0200
@@ -749,7 +749,7 @@
let
val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)
val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes
- (Name.invents (Variable.names_of ctxt') Name.uu (length Ts - length params))
+ (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params))
val params' = (more_names @ param_names) ~~ Ts
in
trace_ex ctxt'' params' atoms (discr initems) n hist
--- a/src/Provers/blast.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Provers/blast.ML Thu Jun 09 23:30:18 2011 +0200
@@ -1234,18 +1234,14 @@
in skoSubgoal 0 (from 0 (discard_foralls t)) end;
-(*Tactic using tableau engine and proof reconstruction.
- "start" is CPU time at start, for printing SEARCH time
- (also prints reconstruction time)
+(*Tableau engine and proof reconstruction operating on subgoal 1.
+ "start" is CPU time at start, for printing SEARCH time (also prints reconstruction time)
"lim" is depth limit.*)
-fun timing_depth_tac start ctxt lim i st0 =
+fun raw_blast start ctxt lim st =
let val thy = Proof_Context.theory_of ctxt
val state = initialize ctxt
val trace = Config.get ctxt trace;
val stats = Config.get ctxt stats;
- val st = st0
- |> rotate_prems (i - 1)
- |> Conv.gconv_rule Object_Logic.atomize_prems 1
val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
@@ -1265,20 +1261,29 @@
end
in
prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
- |> Seq.map (rotate_prems (1 - i))
end
- handle PROVE => Seq.empty | THM _ => Seq.empty;
+ handle PROVE => Seq.empty
+ | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
-(*Public version with fixed depth*)
-fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
+fun depth_tac ctxt lim i st =
+ SELECT_GOAL
+ (Object_Logic.atomize_prems_tac 1 THEN
+ raw_blast (Timing.start ()) ctxt lim) i st;
+
val (depth_limit, setup_depth_limit) =
Attrib.config_int @{binding blast_depth_limit} (K 20);
fun blast_tac ctxt i st =
- ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i
- THEN flexflex_tac) st
- handle TRANS s => (if Config.get ctxt trace then warning ("blast: " ^ s) else (); Seq.empty);
+ let
+ val start = Timing.start ();
+ val lim = Config.get ctxt depth_limit;
+ in
+ SELECT_GOAL
+ (Object_Logic.atomize_prems_tac 1 THEN
+ DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN
+ flexflex_tac) i st
+ end;
--- a/src/Provers/clasimp.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Provers/clasimp.ML Thu Jun 09 23:30:18 2011 +0200
@@ -117,10 +117,6 @@
(* auto_tac *)
-fun blast_depth_tac ctxt m i thm =
- Blast.depth_tac ctxt m i thm
- handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
-
(* a variant of depth_tac that avoids interference of the simplifier
with dup_step_tac when they are combined by auto_tac *)
local
@@ -140,12 +136,12 @@
end;
-(*Designed to be idempotent, except if blast_depth_tac instantiates variables
+(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
in some of the subgoals*)
fun mk_auto_tac ctxt m n =
let
val main_tac =
- blast_depth_tac ctxt m (* fast but can't use wrappers *)
+ Blast.depth_tac ctxt m (* fast but can't use wrappers *)
ORELSE'
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
in
--- a/src/Provers/hypsubst.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Provers/hypsubst.ML Thu Jun 09 23:30:18 2011 +0200
@@ -163,7 +163,7 @@
| t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
val thy = Thm.theory_of_thm rl';
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
- in compose_tac (true, Drule.instantiate (instT,
+ in compose_tac (true, Drule.instantiate_normalize (instT,
map (pairself (cterm_of thy))
[(Var (ixn, Ts ---> U --> body_type T), u),
(Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
--- a/src/Pure/Isar/class.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Isar/class.ML Thu Jun 09 23:30:18 2011 +0200
@@ -426,7 +426,7 @@
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
val tycos = map #1 all_arities;
val (_, sorts, sort) = hd all_arities;
- val vs = Name.names Name.context Name.aT sorts;
+ val vs = Name.invent_names Name.context Name.aT sorts;
in (tycos, vs, sort) end;
--- a/src/Pure/Isar/code.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Isar/code.ML Thu Jun 09 23:30:18 2011 +0200
@@ -433,7 +433,7 @@
in (c, (vs'', binder_types ty')) end;
val c' :: cs' = map (analyze_constructor thy) cs;
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
- val vs = Name.names Name.context Name.aT sorts;
+ val vs = Name.invent_names Name.context Name.aT sorts;
val cs''' = map (inst vs) cs'';
in (tyco, (vs, rev cs''')) end;
@@ -444,7 +444,7 @@
fun get_type thy tyco = case get_type_entry thy tyco
of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
| NONE => arity_number thy tyco
- |> Name.invents Name.context Name.aT
+ |> Name.invent Name.context Name.aT
|> map (rpair [])
|> rpair []
|> rpair false;
@@ -779,7 +779,7 @@
fun inter_sorts vs =
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
val sorts = map_transpose inter_sorts vss;
- val vts = Name.names Name.context Name.aT sorts;
+ val vts = Name.invent_names Name.context Name.aT sorts;
val thms' =
map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
@@ -1145,8 +1145,8 @@
fun case_cong thy case_const (num_args, (pos, _)) =
let
- val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
- val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
+ val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
+ val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
val Ts = binder_types T;
--- a/src/Pure/Isar/obtain.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Jun 09 23:30:18 2011 +0200
@@ -133,7 +133,7 @@
val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
(*obtain statements*)
- val thesisN = Name.variant xs Auto_Bind.thesisN;
+ val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
val that_name = if name = "" then thatN else name;
--- a/src/Pure/Isar/rule_insts.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Thu Jun 09 23:30:18 2011 +0200
@@ -173,7 +173,7 @@
else
Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
in
- Drule.instantiate insts thm |> Rule_Cases.save thm
+ Drule.instantiate_normalize insts thm |> Rule_Cases.save thm
end;
fun read_instantiate_mixed' ctxt (args, concl_args) thm =
@@ -323,7 +323,7 @@
fun liftpair (cv,ct) =
(cterm_fun liftvar cv, cterm_fun liftterm ct)
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
- val rule = Drule.instantiate
+ val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
(Thm.lift_rule (Thm.cprem_of st i) thm)
in
@@ -347,7 +347,7 @@
val maxidx = Thm.maxidx_of rl;
fun cvar xi = cert (Var (xi, propT));
val revcut_rl' =
- instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
+ Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
in
(case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
--- a/src/Pure/Isar/specification.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Isar/specification.ML Thu Jun 09 23:30:18 2011 +0200
@@ -93,7 +93,7 @@
(case duplicates (op =) commons of [] => ()
| dups => error ("Duplicate local variables " ^ commas_quote dups));
val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
- val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
+ val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
--- a/src/Pure/ML/ml_antiquote.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Thu Jun 09 23:30:18 2011 +0200
@@ -29,7 +29,7 @@
fun variant a ctxt =
let
val names = Names.get ctxt;
- val ([b], names') = Name.variants [a] names;
+ val (b, names') = Name.variant a names;
val ctxt' = Names.put names' ctxt;
in (b, ctxt') end;
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 09 23:30:18 2011 +0200
@@ -200,7 +200,7 @@
fun rew_term Ts t =
let
val frees =
- map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
+ map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
val t' = r (subst_bounds (frees, t));
fun strip [] t = t
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
--- a/src/Pure/Proof/proofchecker.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Jun 09 23:30:18 2011 +0200
@@ -100,7 +100,7 @@
| thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
let
- val ([x], names') = Name.variants [s] names;
+ val (x, names') = Name.variant s names;
val thm = thm_of ((x, T) :: vs, names') Hs prf
in
Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
--- a/src/Pure/Syntax/syntax_ext.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Thu Jun 09 23:30:18 2011 +0200
@@ -241,7 +241,7 @@
val rangeT = Term.range_type typ handle Match =>
err_in_mfix "Missing structure argument for indexed syntax" mfix;
- val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
+ val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
val (xs1, xs2) = chop (find_index is_index args) xs;
val i = Ast.Variable "i";
val lhs = Ast.mk_appl (Ast.Constant indexed_const)
--- a/src/Pure/Syntax/syntax_trans.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Thu Jun 09 23:30:18 2011 +0200
@@ -439,7 +439,7 @@
(* dependent / nondependent quantifiers *)
fun var_abs mark (x, T, b) =
- let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
+ let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
in (x', subst_bound (mark (x', T), b)) end;
val variant_abs = var_abs Free;
--- a/src/Pure/axclass.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/axclass.ML Thu Jun 09 23:30:18 2011 +0200
@@ -265,7 +265,7 @@
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
- val names = Name.invents Name.context Name.aT (length Ss);
+ val names = Name.invent Name.context Name.aT (length Ss);
val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
val completions = super_class_completions |> map (fn c1 =>
@@ -445,7 +445,7 @@
val (th', thy') = Global_Theory.store_thm
(Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
- val args = Name.names Name.context Name.aT Ss;
+ val args = Name.invent_names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
--- a/src/Pure/build-jars Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/build-jars Thu Jun 09 23:30:18 2011 +0200
@@ -6,6 +6,53 @@
#
# Requires proper Isabelle settings environment.
+## sources
+
+declare -a SOURCES=(
+ Concurrent/future.scala
+ Concurrent/simple_thread.scala
+ Concurrent/volatile.scala
+ General/exn.scala
+ General/timing.scala
+ General/linear_set.scala
+ General/markup.scala
+ General/position.scala
+ General/pretty.scala
+ General/scan.scala
+ General/sha1.scala
+ General/symbol.scala
+ General/xml.scala
+ General/xml_data.scala
+ General/yxml.scala
+ Isar/keyword.scala
+ Isar/outer_syntax.scala
+ Isar/parse.scala
+ Isar/token.scala
+ PIDE/command.scala
+ PIDE/document.scala
+ PIDE/isar_document.scala
+ PIDE/markup_tree.scala
+ PIDE/text.scala
+ System/cygwin.scala
+ System/download.scala
+ System/event_bus.scala
+ System/gui_setup.scala
+ System/isabelle_process.scala
+ System/isabelle_syntax.scala
+ System/isabelle_system.scala
+ System/platform.scala
+ System/session.scala
+ System/session_manager.scala
+ System/standard_system.scala
+ System/swing_thread.scala
+ Thy/completion.scala
+ Thy/html.scala
+ Thy/thy_header.scala
+ Thy/thy_syntax.scala
+ library.scala
+ package.scala
+)
+
## diagnostics
@@ -61,51 +108,6 @@
## dependencies
-declare -a SOURCES=(
- Concurrent/future.scala
- Concurrent/simple_thread.scala
- Concurrent/volatile.scala
- General/exn.scala
- General/timing.scala
- General/linear_set.scala
- General/markup.scala
- General/position.scala
- General/pretty.scala
- General/scan.scala
- General/sha1.scala
- General/symbol.scala
- General/xml.scala
- General/xml_data.scala
- General/yxml.scala
- Isar/keyword.scala
- Isar/outer_syntax.scala
- Isar/parse.scala
- Isar/token.scala
- PIDE/command.scala
- PIDE/document.scala
- PIDE/isar_document.scala
- PIDE/markup_tree.scala
- PIDE/text.scala
- System/cygwin.scala
- System/download.scala
- System/event_bus.scala
- System/gui_setup.scala
- System/isabelle_process.scala
- System/isabelle_syntax.scala
- System/isabelle_system.scala
- System/platform.scala
- System/session.scala
- System/session_manager.scala
- System/standard_system.scala
- System/swing_thread.scala
- Thy/completion.scala
- Thy/html.scala
- Thy/thy_header.scala
- Thy/thy_syntax.scala
- library.scala
- package.scala
-)
-
TARGET_DIR="$ISABELLE_HOME/lib/classes"
PURE_JAR="$TARGET_DIR/Pure.jar"
FULL_JAR="$TARGET_DIR/isabelle-scala.jar"
--- a/src/Pure/codegen.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/codegen.ML Thu Jun 09 23:30:18 2011 +0200
@@ -273,7 +273,7 @@
fun preprocess_term thy t =
let
- val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
+ val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
(* fake definition *)
val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
fun err () = error "preprocess_term: bad preprocessor"
--- a/src/Pure/conjunction.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/conjunction.ML Thu Jun 09 23:30:18 2011 +0200
@@ -130,7 +130,7 @@
local
fun conjs thy n =
- let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
+ let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
in (As, mk_conjunction_balanced As) end;
val B = read_prop "B";
--- a/src/Pure/conv.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/conv.ML Thu Jun 09 23:30:18 2011 +0200
@@ -162,7 +162,7 @@
val lhs = Thm.lhs_of rule1;
val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
in
- Drule.instantiate (Thm.match (lhs, ct)) rule2
+ Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
end;
--- a/src/Pure/display.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/display.ML Thu Jun 09 23:30:18 2011 +0200
@@ -156,7 +156,7 @@
val tfrees = map (fn v => TFree (v, []));
fun pretty_type syn (t, (Type.LogicalType n)) =
if syn then NONE
- else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
+ else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
| pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
if syn <> syn' then NONE
else SOME (Pretty.block
--- a/src/Pure/drule.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/drule.ML Thu Jun 09 23:30:18 2011 +0200
@@ -24,7 +24,7 @@
val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
- val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
+ val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
val zero_var_indexes_list: thm list -> thm list
val zero_var_indexes: thm -> thm
val implies_intr_hyps: thm -> thm
@@ -110,7 +110,6 @@
val comp_no_flatten: thm * int -> int -> thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
val rename_bvars': string option list -> thm -> thm
- val incr_type_indexes: int -> thm -> thm
val incr_indexes: thm -> thm -> thm
val incr_indexes2: thm -> thm -> thm -> thm
val remdups_rl: thm
@@ -337,7 +336,7 @@
[] => (fth, fn x => x)
| vars =>
let fun newName (Var(ix,_), (pairs,used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
(prop :: Thm.terms_of_tpairs tpairs, [])) vars
@@ -803,13 +802,6 @@
(* var indexes *)
-(*Increment the indexes of only the type variables*)
-fun incr_type_indexes inc th =
- let val tvs = OldTerm.term_tvars (prop_of th)
- and thy = Thm.theory_of_thm th
- fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
- in Thm.instantiate (map inc_tvar tvs, []) th end;
-
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
fun incr_indexes2 th1 th2 =
@@ -829,8 +821,7 @@
(*** Instantiate theorem th, reading instantiations in theory thy ****)
-(*Version that normalizes the result: Thm.instantiate no longer does that*)
-fun instantiate instpair th =
+fun instantiate_normalize instpair th =
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
@@ -862,7 +853,7 @@
let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
in (inst ct, inst cu) end
fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T))
- in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
+ in instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
handle TERM _ =>
raise THM("cterm_instantiate: incompatible theories",0,[th])
| TYPE (msg, _, _) => raise THM(msg, 0, [th])
--- a/src/Pure/logic.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/logic.ML Thu Jun 09 23:30:18 2011 +0200
@@ -253,7 +253,7 @@
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
fun mk_arities (t, Ss, S) =
- let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
+ let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
in map (fn c => mk_of_class (T, c)) S end;
fun dest_arity tm =
@@ -279,7 +279,7 @@
val extra = fold (Sorts.remove_sort o #2) present shyps;
val n = length present;
- val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
+ val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
val present_map =
map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
--- a/src/Pure/more_thm.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/more_thm.ML Thu Jun 09 23:30:18 2011 +0200
@@ -341,7 +341,7 @@
fun stripped_sorts thy t =
let
val tfrees = rev (map TFree (Term.add_tfrees t []));
- val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
+ val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
val strip = tfrees ~~ tfrees';
val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
--- a/src/Pure/name.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/name.ML Thu Jun 09 23:30:18 2011 +0200
@@ -21,12 +21,11 @@
val make_context: string list -> context
val declare: string -> context -> context
val is_declared: context -> string -> bool
- val invents: context -> string -> int -> string list
- val names: context -> string -> 'a list -> (string * 'a) list
+ val invent: context -> string -> int -> string list
+ val invent_names: context -> string -> 'a list -> (string * 'a) list
val invent_list: string list -> string -> int -> string list
- val variants: string list -> context -> string list * context
+ val variant: string -> context -> string * context
val variant_list: string list -> string list -> string list
- val variant: string list -> string -> string
val desymbolize: bool -> string -> string
end;
@@ -95,28 +94,26 @@
fun make_context used = fold declare used context;
-(* invents *)
+(* invent names *)
-fun invents ctxt =
+fun invent ctxt =
let
fun invs _ 0 = []
| invs x n =
- let val x' = Symbol.bump_string x in
- if is_declared ctxt x then invs x' n
- else x :: invs x' (n - 1)
- end;
+ let val x' = Symbol.bump_string x
+ in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
in invs o clean end;
-fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
+fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
-val invent_list = invents o make_context;
+val invent_list = invent o make_context;
(* variants *)
(*makes a variant of a name distinct from already used names in a
context; preserves a suffix of underscores "_"*)
-val variants = fold_map (fn name => fn ctxt =>
+fun variant name ctxt =
let
fun vary x =
(case declared ctxt x of
@@ -134,10 +131,9 @@
|> x0 <> x' ? declare_renaming (x0, x')
|> declare x';
in (x', ctxt') end;
- in (x' ^ replicate_string n "_", ctxt') end);
+ in (x' ^ replicate_string n "_", ctxt') end;
-fun variant_list used names = #1 (make_context used |> variants names);
-fun variant used = singleton (variant_list used);
+fun variant_list used names = #1 (make_context used |> fold_map variant names);
(* names conforming to typical requirements of identifiers in the world outside *)
--- a/src/Pure/proofterm.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/proofterm.ML Thu Jun 09 23:30:18 2011 +0200
@@ -657,7 +657,7 @@
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
- val fmap = fs ~~ #1 (Name.variants (map fst fs) used);
+ val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
fun thaw (f as (a, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
@@ -668,7 +668,7 @@
local
fun new_name (ix, (pairs,used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
@@ -952,7 +952,7 @@
fun canonical_instance typs =
let
- val names = Name.invents Name.context Name.aT (length typs);
+ val names = Name.invent Name.context Name.aT (length typs);
val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
in instantiate (instT, []) end;
--- a/src/Pure/raw_simplifier.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Thu Jun 09 23:30:18 2011 +0200
@@ -305,7 +305,7 @@
fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
let
val names = Term.declare_term_names t Name.context;
- val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
+ val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
--- a/src/Pure/term.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/term.ML Thu Jun 09 23:30:18 2011 +0200
@@ -514,7 +514,8 @@
val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
fun variant_frees t frees =
- fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
+ fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
+ map snd frees;
fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*)
@@ -705,7 +706,7 @@
fun strip_abs t (0, used) = (([], t), (0, used))
| strip_abs (Abs (v, T, t)) (k, used) =
let
- val ([v'], used') = Name.variants [v] used;
+ val (v', used') = Name.variant v used;
val t' = subst_bound (Free (v', T), t);
val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
in (((v', T) :: vs, t''), (k', used'')) end
@@ -713,7 +714,7 @@
fun expand_eta [] t _ = ([], t)
| expand_eta (T::Ts) t used =
let
- val ([v], used') = Name.variants [""] used;
+ val (v, used') = Name.variant "" used;
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
in ((v, T) :: vs, t') end;
val ((vs1, t'), (k', used')) = strip_abs t (k, used);
@@ -936,7 +937,8 @@
| name_clash (Abs (_, _, t)) = name_clash t
| name_clash _ = false;
in
- if name_clash body then dest_abs (Name.variant [x] x, T, body) (*potentially slow*)
+ if name_clash body then
+ dest_abs (singleton (Name.variant_list [x]) x, T, body) (*potentially slow*)
else (x, subst_bound (Free (x, T), body))
end;
@@ -955,7 +957,7 @@
else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
- let val [x] = Name.invents used Name.uu 1
+ 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 =
let val (b', used') = free_dummy_patterns b used
--- a/src/Pure/term_subst.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/term_subst.ML Thu Jun 09 23:30:18 2011 +0200
@@ -163,7 +163,7 @@
fun zero_var_inst vars =
fold (fn v as ((x, i), X) => fn (inst, used) =>
let
- val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
+ val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
vars ([], Name.context) |> #1;
--- a/src/Pure/type.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/type.ML Thu Jun 09 23:30:18 2011 +0200
@@ -345,7 +345,7 @@
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
- val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
+ val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
fun thaw (f as (_, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
@@ -358,7 +358,7 @@
local
fun new_name (ix, (pairs, used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
fun freeze_one alist (ix, sort) =
--- a/src/Pure/type_infer.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/type_infer.ML Thu Jun 09 23:30:18 2011 +0200
@@ -96,7 +96,7 @@
val used =
(fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
- val names = Name.invents used ("?" ^ Name.aT) (length parms);
+ val names = Name.invent used ("?" ^ Name.aT) (length parms);
val tab = Vartab.make (parms ~~ names);
fun finish_typ T =
@@ -117,7 +117,7 @@
fun subst_param (xi, S) (inst, used) =
if is_param xi then
let
- val [a] = Name.invents used Name.aT 1;
+ val [a] = Name.invent used Name.aT 1;
val used' = Name.declare a used;
in (((xi, S), TFree (a, S)) :: inst, used') end
else (inst, used);
--- a/src/Pure/variable.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Pure/variable.ML Thu Jun 09 23:30:18 2011 +0200
@@ -255,7 +255,7 @@
fun variant_frees ctxt ts frees =
let
val names = names_of (fold declare_names ts ctxt);
- val xs = fst (Name.variants (map #1 frees) names);
+ val xs = fst (fold_map Name.variant (map #1 frees) names);
in xs ~~ map snd frees end;
@@ -365,7 +365,7 @@
val xs = map check_name bs;
val names = names_of ctxt;
val (xs', names') =
- if is_body ctxt then Name.variants xs names |>> map Name.skolem
+ if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
else (xs, fold Name.declare xs names);
in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
@@ -373,7 +373,7 @@
let
val names = names_of ctxt;
val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
- val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
+ val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
end;
@@ -391,7 +391,7 @@
fun invent_types Ss ctxt =
let
- val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
+ val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
in (tfrees, ctxt') end;
--- a/src/Tools/Code/code_haskell.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Jun 09 23:30:18 2011 +0200
@@ -264,13 +264,12 @@
let
fun namify_fun upper base (nsp_fun, nsp_typ) =
let
- val (base', nsp_fun') = yield_singleton Name.variants
- (if upper then first_upper base else base) nsp_fun;
+ val (base', nsp_fun') =
+ Name.variant (if upper then first_upper base else base) nsp_fun;
in (base', (nsp_fun', nsp_typ)) end;
fun namify_typ base (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = yield_singleton Name.variants
- (first_upper base) nsp_typ
+ val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
in (base', (nsp_fun, nsp_typ')) end;
fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
--- a/src/Tools/Code/code_ml.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jun 09 23:30:18 2011 +0200
@@ -716,12 +716,12 @@
let
fun namify_const upper base (nsp_const, nsp_type) =
let
- val (base', nsp_const') = yield_singleton Name.variants
- (if upper then first_upper base else base) nsp_const
+ val (base', nsp_const') =
+ Name.variant (if upper then first_upper base else base) nsp_const
in (base', (nsp_const', nsp_type)) end;
fun namify_type base (nsp_const, nsp_type) =
let
- val (base', nsp_type') = yield_singleton Name.variants base nsp_type
+ val (base', nsp_type') = Name.variant base nsp_type
in (base', (nsp_const, nsp_type')) end;
fun namify_stmt (Code_Thingol.Fun _) = namify_const false
| namify_stmt (Code_Thingol.Datatype _) = namify_type
--- a/src/Tools/Code/code_namespace.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_namespace.ML Thu Jun 09 23:30:18 2011 +0200
@@ -46,8 +46,7 @@
let
fun alias_fragments name = case module_alias name
of SOME name' => Long_Name.explode name'
- | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
- (Long_Name.explode name);
+ | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
in
fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
--- a/src/Tools/Code/code_printer.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jun 09 23:30:18 2011 +0200
@@ -165,7 +165,7 @@
fun intro_vars names (namemap, namectxt) =
let
- val (names', namectxt') = Name.variants names namectxt;
+ val (names', namectxt') = fold_map Name.variant names namectxt;
val namemap' = fold2 (curry Symtab.update) names names' namemap;
in (namemap', namectxt') end;
@@ -184,9 +184,9 @@
fun fillup_param _ (_, SOME v) = v
| fillup_param x (i, NONE) = x ^ string_of_int i;
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
- val x = Name.variant (map_filter I fished1) "x";
+ val x = singleton (Name.variant_list (map_filter I fished1)) "x";
val fished2 = map_index (fillup_param x) fished1;
- val (fished3, _) = Name.variants fished2 Name.context;
+ val (fished3, _) = fold_map Name.variant fished2 Name.context;
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
--- a/src/Tools/Code/code_scala.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Jun 09 23:30:18 2011 +0200
@@ -149,7 +149,7 @@
fun print_def name (vs, ty) [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
- val params = Name.invents (snd reserved) "a" (length tys);
+ val params = Name.invent (snd reserved) "a" (length tys);
val tyvars = intro_tyvars vs reserved;
val vars = intro_vars params reserved;
in
@@ -214,7 +214,7 @@
(fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
(applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
["final", "case", "class", deresolve co]) vs_args)
- (Name.names (snd reserved) "a" tys),
+ (Name.invent_names (snd reserved) "a" tys),
str "extends",
applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
((str o deresolve) name) vs
@@ -238,9 +238,9 @@
fun print_classparam_def (classparam, ty) =
let
val (tys, ty) = Code_Thingol.unfold_fun ty;
- val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
+ val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1;
val proto_vars = intro_vars [implicit_name] reserved;
- val auxs = Name.invents (snd proto_vars) "a" (length tys);
+ val auxs = Name.invent (snd proto_vars) "a" (length tys);
val vars = intro_vars auxs proto_vars;
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
@@ -267,7 +267,7 @@
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
let
- val aux_tys = Name.names (snd reserved) "a" tys;
+ val aux_tys = Name.invent_names (snd reserved) "a" tys;
val auxs = map fst aux_tys;
val vars = intro_vars auxs reserved;
val aux_abstr = if null auxs then [] else [enum "," "(" ")"
@@ -294,16 +294,16 @@
in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
fun namify_class base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_class') = yield_singleton Name.variants base nsp_class
+ val (base', nsp_class') = Name.variant base nsp_class
in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
fun namify_object base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_object') = yield_singleton Name.variants base nsp_object
+ val (base', nsp_object') = Name.variant base nsp_object
in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
let
val (base', nsp_common') =
- yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
+ Name.variant (if upper then first_upper base else base) nsp_common
in
(base',
((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
--- a/src/Tools/Code/code_target.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_target.ML Thu Jun 09 23:30:18 2011 +0200
@@ -416,7 +416,7 @@
let
val _ = if Code_Thingol.contains_dict_var t then
error "Term to be evaluated contains free dictionaries" else ();
- val v' = Name.variant (map fst vs) "a";
+ val v' = singleton (Name.variant_list (map fst vs)) "a";
val vs' = (v', []) :: vs;
val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
val value_name = "Value.value.value"
--- a/src/Tools/Code/code_thingol.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jun 09 23:30:18 2011 +0200
@@ -237,7 +237,7 @@
| unfold_abs_eta tys t =
let
val ctxt = fold_varnames Name.declare t Name.context;
- val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
+ val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
fun eta_expand k (c as (name, (_, tys)), ts) =
@@ -248,7 +248,7 @@
then error ("Impossible eta-expansion for constant " ^ quote name) else ();
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = (map o apfst) SOME
- (Name.names ctxt "a" ((take l o drop j) tys));
+ (Name.invent_names ctxt "a" ((take l o drop j) tys));
in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dict_var t =
@@ -354,7 +354,7 @@
fun add_variant update (thing, name) (tab, used) =
let
- val (name', used') = yield_singleton Name.variants name used;
+ val (name', used') = Name.variant name used;
val tab' = update (thing, name') tab;
in (tab', used') end;
@@ -671,7 +671,7 @@
val classparams = these_classparams class;
val further_classparams = maps these_classparams
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
- val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
+ val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
@@ -820,7 +820,7 @@
val k = length ts;
val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
- val vs = Name.names ctxt "a" tys;
+ val vs = Name.invent_names ctxt "a" tys;
in
fold_map (translate_typ thy algbr eqngr permissive) tys
##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
--- a/src/Tools/Code/lib/Tools/codegen Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Thu Jun 09 23:30:18 2011 +0200
@@ -51,7 +51,7 @@
## invoke code generation
FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
- (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
+ (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
handle _ => OS.Process.exit OS.Process.failure;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
--- a/src/Tools/IsaPlanner/isand.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Thu Jun 09 23:30:18 2011 +0200
@@ -190,7 +190,7 @@
val tvars = List.foldr OldTerm.add_term_tvars [] ts;
val (names',renamings) =
List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
- let val n2 = Name.variant Ns n in
+ let val n2 = singleton (Name.variant_list Ns) n in
(n2::Ns, (tv, (n2,s))::Rs)
end) (tfree_names @ names,[]) tvars;
in renamings end;
@@ -223,7 +223,7 @@
val Ns = List.foldr OldTerm.add_term_names names ts;
val (_,renamings) =
Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
- let val n2 = Name.variant Ns n in
+ let val n2 = singleton (Name.variant_list Ns) n in
(n2 :: Ns, (v, (n2,ty)) :: Rs)
end) ((Ns,[]), vars);
in renamings end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Jun 09 23:30:18 2011 +0200
@@ -101,7 +101,7 @@
val names = usednames_of_thm rule;
val (fromnames,tonames,names2,Ts') =
Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
- let val n2 = Name.variant names n in
+ let val n2 = singleton (Name.variant_list names) n in
(ctermify (Free(faken,ty)) :: rnf,
ctermify (Free(n2,ty)) :: rnt,
n2 :: names,
@@ -146,7 +146,7 @@
val vars_to_fix = union (op =) termvars cond_vs;
val (renamings, names2) =
List.foldr (fn (((n,i),ty), (vs, names')) =>
- let val n' = Name.variant names' n in
+ let val n' = singleton (Name.variant_list names') n in
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
end)
([], names) vars_to_fix;
@@ -154,7 +154,7 @@
(* make a new fresh typefree instantiation for the given tvar *)
fun new_tfree (tv as (ix,sort), (pairs,used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
--- a/src/Tools/eqsubst.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/eqsubst.ML Thu Jun 09 23:30:18 2011 +0200
@@ -179,7 +179,7 @@
fun fakefree_badbounds Ts t =
let val (FakeTs,Ts,newnames) =
List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
- let val newname = Name.variant usednames n
+ let val newname = singleton (Name.variant_list usednames) n
in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
(newname,ty)::Ts,
newname::usednames) end)
--- a/src/Tools/induct.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/induct.ML Thu Jun 09 23:30:18 2011 +0200
@@ -588,9 +588,10 @@
val concl = Logic.strip_assums_concl goal;
in
Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
- |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
+ |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
end
- end handle General.Subscript => Seq.empty;
+ end
+ handle General.Subscript => Seq.empty;
end;
@@ -692,7 +693,7 @@
| add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
| add (SOME (NONE, (t, _))) ctxt =
let
- val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
+ val (s, _) = Name.variant "x" (Variable.names_of ctxt);
val ([(lhs, (_, th))], ctxt') =
Local_Defs.add_defs [((Binding.name s, NoSyn),
(Thm.empty_binding, t))] ctxt
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jun 09 23:30:18 2011 +0200
@@ -7,7 +7,7 @@
## sources
-declare -a SOURCE_FILES=(
+declare -a SOURCES=(
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
@@ -25,7 +25,7 @@
"src/session_dockable.scala"
)
-declare -a MORE_FILES=(
+declare -a RESOURCES=(
"src/actions.xml"
"src/dockables.xml"
"src/Isabelle.props"
@@ -169,7 +169,7 @@
OUTDATED=true
else
OUTDATED=false
- for SOURCE in "${SOURCE_FILES[@]}" "${MORE_FILES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
+ for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
do
[ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
[ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
@@ -198,7 +198,7 @@
mkdir -p dist dist/classes || failed
cp -a "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
- cp -a "${MORE_FILES[@]}" dist/classes/.
+ cp -a "${RESOURCES[@]}" dist/classes/.
cp src/jEdit.props dist/properties/.
cp -a src/modes/. dist/modes/.
@@ -218,7 +218,7 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
exec "$SCALA_HOME/bin/scalac" -unchecked -deprecation \
- -d dist/classes -target:jvm-1.5 "${SOURCE_FILES[@]}"
+ -d dist/classes -target:jvm-1.5 "${SOURCES[@]}"
) || fail "Failed to compile sources"
cd dist/classes
--- a/src/Tools/nbe.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/Tools/nbe.ML Thu Jun 09 23:30:18 2011 +0200
@@ -330,7 +330,8 @@
val vs = (fold o Code_Thingol.fold_varnames)
(fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
val names = Name.make_context (map fst vs);
- fun declare v k ctxt = let val vs = Name.invents ctxt v k
+ fun declare v k ctxt =
+ let val vs = Name.invent ctxt v k
in (vs, fold Name.declare vs ctxt) end;
val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
then declare v (k - 1) #>> (fn vs => (v, vs))
@@ -372,7 +373,7 @@
fun assemble_eqns (c, (num_args, (dicts, eqns))) =
let
val default_args = map nbe_default
- (Name.invent_list [] "a" (num_args - length dicts));
+ (Name.invent Name.context "a" (num_args - length dicts));
val eqns' = map_index (assemble_eqn c dicts default_args) eqns
@ (if c = "" then [] else [(nbe_fun (length eqns) c,
[([ml_list (rev (dicts @ default_args))],
@@ -421,7 +422,7 @@
| eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
let
val names = map snd super_classes @ map fst classparams;
- val params = Name.invent_list [] "d" (length names);
+ val params = Name.invent Name.context "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
[([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
--- a/src/ZF/Tools/cartprod.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/ZF/Tools/cartprod.ML Thu Jun 09 23:30:18 2011 +0200
@@ -108,7 +108,7 @@
val newt = ap_split T1 T2 (Var(v,T'))
val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
in
- remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
+ remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
cterm newt)]) rl)
end
| split_rule_var (t,T,rl) = rl;
--- a/src/ZF/Tools/inductive_package.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Jun 09 23:30:18 2011 +0200
@@ -96,7 +96,7 @@
Syntax.string_of_term ctxt t);
(*** Construct the fixedpoint definition ***)
- val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
+ val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
@@ -493,7 +493,7 @@
The name "x.1" comes from the "RS spec" !*)
val inst =
case elem_frees of [_] => I
- | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
+ | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
cterm_of thy1 elem_tuple)]);
(*strip quantifier and the implication*)
--- a/src/ZF/Tools/primrec_package.ML Thu Jun 09 15:14:21 2011 +0200
+++ b/src/ZF/Tools/primrec_package.ML Thu Jun 09 23:30:18 2011 +0200
@@ -139,8 +139,9 @@
(** make definition **)
(*the recursive argument*)
- val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
- Ind_Syntax.iT)
+ val rec_arg =
+ Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
+ Ind_Syntax.iT)
val def_tm = Logic.mk_equals
(subst_bound (rec_arg, fabs),