merged
authorwenzelm
Thu Jun 09 23:30:18 2011 +0200 (2011-06-09)
changeset 43345165188299a25
parent 43344 b017cfb10df4
parent 43333 2bdec7f430d3
child 43346 911cb8242dfe
child 43351 b19d95b4d736
merged
src/Tools/Code/code_ml.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Jun 09 15:14:21 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Jun 09 23:30:18 2011 +0200
     1.3 @@ -854,8 +854,8 @@
     1.4    @{index_ML_type Name.context} \\
     1.5    @{index_ML Name.context: Name.context} \\
     1.6    @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
     1.7 -  @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
     1.8 -  @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
     1.9 +  @{index_ML Name.invent: "Name.context -> string -> int -> string list"} \\
    1.10 +  @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
    1.11    \end{mldecls}
    1.12    \begin{mldecls}
    1.13    @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\
    1.14 @@ -875,11 +875,11 @@
    1.15    \item @{ML Name.declare}~@{text "name"} enters a used name into the
    1.16    context.
    1.17  
    1.18 -  \item @{ML Name.invents}~@{text "context name n"} produces @{text
    1.19 +  \item @{ML Name.invent}~@{text "context name n"} produces @{text
    1.20    "n"} fresh names derived from @{text "name"}.
    1.21  
    1.22 -  \item @{ML Name.variants}~@{text "names context"} produces fresh
    1.23 -  variants of @{text "names"}; the result is entered into the context.
    1.24 +  \item @{ML Name.variant}~@{text "name context"} produces a fresh
    1.25 +  variant of @{text "name"}; the result is declared to the context.
    1.26  
    1.27    \item @{ML Variable.names_of}~@{text "ctxt"} retrieves the context
    1.28    of declared type and term variable names.  Projecting a proof
    1.29 @@ -897,11 +897,11 @@
    1.30    fresh names from the initial @{ML Name.context}. *}
    1.31  
    1.32  ML {*
    1.33 -  val list1 = Name.invents Name.context "a" 5;
    1.34 +  val list1 = Name.invent Name.context "a" 5;
    1.35    @{assert} (list1 = ["a", "b", "c", "d", "e"]);
    1.36  
    1.37    val list2 =
    1.38 -    #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
    1.39 +    #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context);
    1.40    @{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
    1.41  *}
    1.42  
    1.43 @@ -914,11 +914,11 @@
    1.44  ML {*
    1.45    val names = Variable.names_of @{context};
    1.46  
    1.47 -  val list1 = Name.invents names "a" 5;
    1.48 +  val list1 = Name.invent names "a" 5;
    1.49    @{assert} (list1 = ["d", "e", "f", "g", "h"]);
    1.50  
    1.51    val list2 =
    1.52 -    #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
    1.53 +    #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] names);
    1.54    @{assert} (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]);
    1.55  *}
    1.56  
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Jun 09 15:14:21 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Jun 09 23:30:18 2011 +0200
     2.3 @@ -1254,8 +1254,8 @@
     2.4    \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
     2.5    \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
     2.6    \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
     2.7 -  \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
     2.8 -  \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
     2.9 +  \indexdef{}{ML}{Name.invent}\verb|Name.invent: Name.context -> string -> int -> string list| \\
    2.10 +  \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\
    2.11    \end{mldecls}
    2.12    \begin{mldecls}
    2.13    \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\
    2.14 @@ -1275,10 +1275,10 @@
    2.15    \item \verb|Name.declare|~\isa{name} enters a used name into the
    2.16    context.
    2.17  
    2.18 -  \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
    2.19 +  \item \verb|Name.invent|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
    2.20  
    2.21 -  \item \verb|Name.variants|~\isa{names\ context} produces fresh
    2.22 -  variants of \isa{names}; the result is entered into the context.
    2.23 +  \item \verb|Name.variant|~\isa{name\ context} produces a fresh
    2.24 +  variant of \isa{name}; the result is declared to the context.
    2.25  
    2.26    \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context
    2.27    of declared type and term variable names.  Projecting a proof
    2.28 @@ -1325,7 +1325,7 @@
    2.29  \isatagML
    2.30  \isacommand{ML}\isamarkupfalse%
    2.31  \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
    2.32 -\ \ 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
    2.33 +\ \ 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
    2.34  \ \ %
    2.35  \isaantiq
    2.36  assert{}%
    2.37 @@ -1333,7 +1333,7 @@
    2.38  \ {\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
    2.39  \isanewline
    2.40  \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
    2.41 -\ \ \ \ {\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
    2.42 +\ \ \ \ {\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
    2.43  \ \ %
    2.44  \isaantiq
    2.45  assert{}%
    2.46 @@ -1370,7 +1370,7 @@
    2.47  \endisaantiq
    2.48  {\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.49  \isanewline
    2.50 -\ \ 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
    2.51 +\ \ 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
    2.52  \ \ %
    2.53  \isaantiq
    2.54  assert{}%
    2.55 @@ -1378,7 +1378,7 @@
    2.56  \ {\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
    2.57  \isanewline
    2.58  \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
    2.59 -\ \ \ \ {\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
    2.60 +\ \ \ \ {\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
    2.61  \ \ %
    2.62  \isaantiq
    2.63  assert{}%
     3.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Thu Jun 09 15:14:21 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Jun 09 23:30:18 2011 +0200
     3.3 @@ -961,7 +961,11 @@
     3.4    ones it cannot prove.  Occasionally, attempting to prove the hard
     3.5    ones may take a long time.
     3.6  
     3.7 -  %FIXME auto nat arguments
     3.8 +  The optional depth arguments in @{text "(auto m n)"} refer to its
     3.9 +  builtin classical reasoning procedures: @{text m} (default 4) is for
    3.10 +  @{method blast}, which is tried first, and @{text n} (default 2) is
    3.11 +  for a slower but more general alternative that also takes wrappers
    3.12 +  into account.
    3.13  
    3.14    \item @{method force} is intended to prove the first subgoal
    3.15    completely, using many fancy proof tools and performing a rather
     4.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jun 09 15:14:21 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jun 09 23:30:18 2011 +0200
     4.3 @@ -1513,7 +1513,11 @@
     4.4    ones it cannot prove.  Occasionally, attempting to prove the hard
     4.5    ones may take a long time.
     4.6  
     4.7 -  %FIXME auto nat arguments
     4.8 +  The optional depth arguments in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}auto\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} refer to its
     4.9 +  builtin classical reasoning procedures: \isa{m} (default 4) is for
    4.10 +  \hyperlink{method.blast}{\mbox{\isa{blast}}}, which is tried first, and \isa{n} (default 2) is
    4.11 +  for a slower but more general alternative that also takes wrappers
    4.12 +  into account.
    4.13  
    4.14    \item \hyperlink{method.force}{\mbox{\isa{force}}} is intended to prove the first subgoal
    4.15    completely, using many fancy proof tools and performing a rather
     5.1 --- a/lib/texinputs/isabelle.sty	Thu Jun 09 15:14:21 2011 +0200
     5.2 +++ b/lib/texinputs/isabelle.sty	Thu Jun 09 23:30:18 2011 +0200
     5.3 @@ -15,17 +15,26 @@
     5.4  \newcommand{\isastyletxt}{\rm}
     5.5  \newcommand{\isastylecmt}{\rm}
     5.6  
     5.7 +\newcommand{\isaspacing}{%
     5.8 +  \sfcode 42 1000 % .
     5.9 +  \sfcode 63 1000 % ?
    5.10 +  \sfcode 33 1000 % !
    5.11 +  \sfcode 58 1000 % :
    5.12 +  \sfcode 59 1000 % ;
    5.13 +  \sfcode 44 1000 % ,
    5.14 +}
    5.15 +
    5.16  %symbol markup -- \emph achieves decent spacing via italic corrections
    5.17  \newcommand{\isamath}[1]{\emph{$#1$}}
    5.18  \newcommand{\isatext}[1]{\emph{#1}}
    5.19 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    5.20 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
    5.21  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    5.22  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    5.23  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    5.24  \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    5.25 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
    5.26 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
    5.27  \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    5.28 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
    5.29 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
    5.30  \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
    5.31  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    5.32  \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
    5.33 @@ -40,13 +49,13 @@
    5.34  \isamarkuptrue\par%
    5.35  \isa@parindent\parindent\parindent0pt%
    5.36  \isa@parskip\parskip\parskip0pt%
    5.37 -\isastyle}{\par}
    5.38 +\isaspacing\isastyle}{\par}
    5.39  
    5.40  \newenvironment{isabelle}
    5.41  {\begin{trivlist}\begin{isabellebody}\item\relax}
    5.42  {\end{isabellebody}\end{trivlist}}
    5.43  
    5.44 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    5.45 +\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
    5.46  
    5.47  \newcommand{\isaindent}[1]{\hphantom{#1}}
    5.48  \newcommand{\isanewline}{\mbox{}\par\mbox{}}
     6.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jun 09 15:14:21 2011 +0200
     6.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jun 09 23:30:18 2011 +0200
     6.3 @@ -86,7 +86,7 @@
     6.4          SOME type_name => (((name, type_name), log_ex name type_name), thy)
     6.5        | NONE =>
     6.6            let
     6.7 -            val args = map (rpair dummyS) (Name.invents Name.context "'a" arity)
     6.8 +            val args = map (rpair dummyS) (Name.invent Name.context "'a" arity)
     6.9              val (T, thy') =
    6.10                Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
    6.11              val type_name = fst (Term.dest_Type T)
    6.12 @@ -446,8 +446,7 @@
    6.13        val nctxt = Name.make_context (duplicates (op =) (names_of t []))
    6.14  
    6.15        fun fresh (i, nctxt) = (position_prefix ^ string_of_int i, (i+1, nctxt))
    6.16 -      fun renamed n (i, nctxt) =
    6.17 -        yield_singleton Name.variants n nctxt ||> pair i
    6.18 +      fun renamed n (i, nctxt) = Name.variant n nctxt ||> pair i
    6.19        fun mk_label (name, t) = @{term assert_at} $ Free (name, @{typ bool}) $ t
    6.20  
    6.21        fun unique t =
    6.22 @@ -472,11 +471,11 @@
    6.23          all_names
    6.24          |> map_filter (try (fn n => (n, short_var_name n)))
    6.25          |> split_list
    6.26 -        ||>> (fn names => Name.variants names (Name.make_context all_names))
    6.27 +        ||>> (fn names => fold_map Name.variant names (Name.make_context all_names))
    6.28          |>> Symtab.make o (op ~~)
    6.29  
    6.30        fun rename_free n = the_default n (Symtab.lookup names n)
    6.31 -      fun rename_abs n = yield_singleton Name.variants (short_var_name n)
    6.32 +      fun rename_abs n = Name.variant (short_var_name n)
    6.33  
    6.34        fun rename _ (Free (n, T)) = Free (rename_free n, T)
    6.35          | rename nctxt (Abs (n, T, t)) =
     7.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jun 09 15:14:21 2011 +0200
     7.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jun 09 23:30:18 2011 +0200
     7.3 @@ -67,8 +67,8 @@
     7.4     fun fw mi th th' th'' =
     7.5       let
     7.6        val th0 = if mi then
     7.7 -           instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
     7.8 -        else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
     7.9 +           Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    7.10 +        else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    7.11       in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    7.12    in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    7.13        fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    7.14 @@ -114,11 +114,11 @@
    7.15     val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
    7.16          pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
    7.17     val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
    7.18 -        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
    7.19 +        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
    7.20     val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
    7.21 -        npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
    7.22 +        npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
    7.23     val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
    7.24 -        ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
    7.25 +        ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
    7.26  
    7.27     fun decomp_mpinf fm =
    7.28       case term_of fm of
     8.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jun 09 15:14:21 2011 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jun 09 23:30:18 2011 +0200
     8.3 @@ -403,7 +403,7 @@
     8.4  
     8.5      (* calculate function arguments of case combinator *)
     8.6      val tns = map fst (Term.add_tfreesT lhsT [])
     8.7 -    val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
     8.8 +    val resultT = TFree (singleton (Name.variant_list tns) "'t", @{sort pcpo})
     8.9      fun fTs T = map (fn (_, args) => map snd args -->> T) spec
    8.10      val fns = Datatype_Prop.indexify_names (map (K "f") spec)
    8.11      val fs = map Free (fns ~~ fTs resultT)
    8.12 @@ -768,7 +768,7 @@
    8.13      val resultT : typ =
    8.14        let
    8.15          val ts : string list = map fst (Term.add_tfreesT lhsT [])
    8.16 -        val t : string = Name.variant ts "'t"
    8.17 +        val t : string = singleton (Name.variant_list ts) "'t"
    8.18        in TFree (t, @{sort pcpo}) end
    8.19  
    8.20      (* define match combinators *)
     9.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Thu Jun 09 15:14:21 2011 +0200
     9.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Thu Jun 09 23:30:18 2011 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4  
     9.5  fun trans_rules name2 name1 n mx =
     9.6    let
     9.7 -    val vnames = Name.invents Name.context "a" n
     9.8 +    val vnames = Name.invent Name.context "a" n
     9.9      val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
    9.10    in
    9.11      [Syntax.Parse_Print_Rule
    10.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 15:14:21 2011 +0200
    10.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 23:30:18 2011 +0200
    10.3 @@ -234,7 +234,7 @@
    10.4            in comp_con T f rhs' (v::vs) taken' end
    10.5        | Const (c, cT) =>
    10.6            let
    10.7 -            val n = Name.variant taken "v"
    10.8 +            val n = singleton (Name.variant_list taken) "v"
    10.9              val v = Free(n, T)
   10.10              val m = Const(match_name c, matcherT (cT, fastype_of rhs))
   10.11              val k = big_lambdas vs rhs
    11.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Jun 09 15:14:21 2011 +0200
    11.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Jun 09 23:30:18 2011 +0200
    11.3 @@ -531,7 +531,7 @@
    11.4      (* prove strictness and reduction rules of pattern combinators *)
    11.5      local
    11.6        val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
    11.7 -      val rn = Name.variant tns "'r";
    11.8 +      val rn = singleton (Name.variant_list tns) "'r";
    11.9        val R = TFree (rn, @{sort pcpo});
   11.10        fun pat_lhs (pat, args) =
   11.11          let
    12.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 15:14:21 2011 +0200
    12.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 23:30:18 2011 +0200
    12.3 @@ -618,7 +618,6 @@
    12.4  open Code_Thingol;
    12.5  
    12.6  fun imp_program naming =
    12.7 -
    12.8    let
    12.9      fun is_const c = case lookup_const naming c
   12.10       of SOME c' => (fn c'' => c' = c'')
   12.11 @@ -635,7 +634,7 @@
   12.12        | dest_abs (t, ty) =
   12.13            let
   12.14              val vs = fold_varnames cons t [];
   12.15 -            val v = Name.variant vs "x";
   12.16 +            val v = singleton (Name.variant_list vs) "x";
   12.17              val ty' = (hd o fst o unfold_fun) ty;
   12.18            in ((SOME v, ty'), t `$ IVar (SOME v)) end;
   12.19      fun force (t as IConst (c, _) `$ t') = if is_return c
    13.1 --- a/src/HOL/Import/hol4rews.ML	Thu Jun 09 15:14:21 2011 +0200
    13.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Jun 09 23:30:18 2011 +0200
    13.3 @@ -605,7 +605,7 @@
    13.4                  then F defname                 (* name_def *)
    13.5                  else if not (member (op =) used pdefname)
    13.6                  then F pdefname                (* name_primdef *)
    13.7 -                else F (Name.variant used pdefname) (* last resort *)
    13.8 +                else F (singleton (Name.variant_list used) pdefname) (* last resort *)
    13.9              end
   13.10      end
   13.11  
    14.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jun 09 15:14:21 2011 +0200
    14.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jun 09 23:30:18 2011 +0200
    14.3 @@ -1419,7 +1419,7 @@
    14.4                                  | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
    14.5                               ))
    14.6                           (zip tys_before tys_after)
    14.7 -        val res = Drule.instantiate (tyinst,[]) th1
    14.8 +        val res = Drule.instantiate_normalize (tyinst,[]) th1
    14.9          val hth = HOLThm([],res)
   14.10          val res = norm_hthm thy hth
   14.11          val _ = message "RESULT:"
    15.1 --- a/src/HOL/Import/shuffler.ML	Thu Jun 09 15:14:21 2011 +0200
    15.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jun 09 23:30:18 2011 +0200
    15.3 @@ -228,7 +228,7 @@
    15.4          val (type_inst,_) =
    15.5              fold (fn (w as (v,_), S) => fn (inst, used) =>
    15.6                        let
    15.7 -                          val v' = Name.variant used v
    15.8 +                          val v' = singleton (Name.variant_list used) v
    15.9                        in
   15.10                            ((w,TFree(v',S))::inst,v'::used)
   15.11                        end)
   15.12 @@ -249,7 +249,7 @@
   15.13          val mid =
   15.14              case rens of
   15.15                  [] => thm'
   15.16 -              | [((_, S), idx)] => instantiate
   15.17 +              | [((_, S), idx)] => Drule.instantiate_normalize
   15.18              ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
   15.19                | _ => error "Shuffler.inst_tfrees internal error"
   15.20      in
   15.21 @@ -298,7 +298,7 @@
   15.22                then
   15.23                    let
   15.24                        val cert = cterm_of thy
   15.25 -                      val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
   15.26 +                      val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT)
   15.27                        val cv = cert v
   15.28                        val ct = cert t
   15.29                        val th = (Thm.assume ct)
   15.30 @@ -361,7 +361,7 @@
   15.31                        Type("fun",[aT,bT]) =>
   15.32                        let
   15.33                            val cert = cterm_of thy
   15.34 -                          val vname = Name.variant (Term.add_free_names t []) "v"
   15.35 +                          val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
   15.36                            val v = Free(vname,aT)
   15.37                            val cv = cert v
   15.38                            val ct = cert t
    16.1 --- a/src/HOL/Inductive.thy	Thu Jun 09 15:14:21 2011 +0200
    16.2 +++ b/src/HOL/Inductive.thy	Thu Jun 09 23:30:18 2011 +0200
    16.3 @@ -295,7 +295,8 @@
    16.4  let
    16.5    fun fun_tr ctxt [cs] =
    16.6      let
    16.7 -      val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
    16.8 +      (* FIXME proper name context!? *)
    16.9 +      val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
   16.10        val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
   16.11      in lambda x ft end
   16.12  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    17.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 15:14:21 2011 +0200
    17.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 23:30:18 2011 +0200
    17.3 @@ -113,8 +113,8 @@
    17.4  
    17.5  fun remove_suc thy thms =
    17.6    let
    17.7 -    val vname = Name.variant (map fst
    17.8 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
    17.9 +    val vname = singleton (Name.variant_list (map fst
   17.10 +      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
   17.11      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
   17.12      fun lhs_of th = snd (Thm.dest_comb
   17.13        (fst (Thm.dest_comb (cprop_of th))));
   17.14 @@ -166,8 +166,8 @@
   17.15  
   17.16  fun remove_suc_clause thy thms =
   17.17    let
   17.18 -    val vname = Name.variant (map fst
   17.19 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
   17.20 +    val vname = singleton (Name.variant_list (map fst
   17.21 +      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
   17.22      fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
   17.23        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   17.24        | find_var _ = NONE;
    18.1 --- a/src/HOL/Library/reflection.ML	Thu Jun 09 15:14:21 2011 +0200
    18.2 +++ b/src/HOL/Library/reflection.ML	Thu Jun 09 23:30:18 2011 +0200
    18.3 @@ -157,7 +157,7 @@
    18.4                   map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    18.5                val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    18.6              in ((fts ~~ (replicate (length fts) ctxt),
    18.7 -                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
    18.8 +                 Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
    18.9              end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
   18.10        end;
   18.11  
   18.12 @@ -230,7 +230,7 @@
   18.13              val substt =
   18.14                let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
   18.15                in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts)  end
   18.16 -            val th = (instantiate (subst_ty, substt)  eq) RS sym
   18.17 +            val th = (Drule.instantiate_normalize (subst_ty, substt)  eq) RS sym
   18.18            in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
   18.19            handle Pattern.MATCH => tryeqs eqs bds)
   18.20        in tryeqs (filter isat eqs) bds end), bds);
   18.21 @@ -277,7 +277,7 @@
   18.22      val cert = cterm_of (Proof_Context.theory_of ctxt)
   18.23      val cvs = map (fn (v as Var(n,t)) => (cert v,
   18.24                    the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
   18.25 -    val th' = instantiate ([], cvs) th
   18.26 +    val th' = Drule.instantiate_normalize ([], cvs) th
   18.27      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
   18.28      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
   18.29                 (fn _ => simp_tac (simpset_of ctxt) 1)
    19.1 --- a/src/HOL/List.thy	Thu Jun 09 15:14:21 2011 +0200
    19.2 +++ b/src/HOL/List.thy	Thu Jun 09 23:30:18 2011 +0200
    19.3 @@ -383,7 +383,8 @@
    19.4  
    19.5    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
    19.6      let
    19.7 -      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
    19.8 +      (* FIXME proper name context!? *)
    19.9 +      val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
   19.10        val e = if opti then singl e else e;
   19.11        val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
   19.12        val case2 =
    20.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jun 09 15:14:21 2011 +0200
    20.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jun 09 23:30:18 2011 +0200
    20.3 @@ -306,7 +306,7 @@
    20.4          (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
    20.5  
    20.6    in fst (RealArith.real_linear_prover translator
    20.7 -        (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
    20.8 +        (map (fn t => Drule.instantiate_normalize ([(tv_n, ctyp_of_term t)],[]) pth_zero)
    20.9              zerodests,
   20.10          map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
   20.11                         arg_conv (arg_conv real_poly_conv))) ges',
   20.12 @@ -343,7 +343,7 @@
   20.13    val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
   20.14    val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
   20.15    val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   20.16 -  val th12 = instantiate ([], cps) th11
   20.17 +  val th12 = Drule.instantiate_normalize ([], cps) th11
   20.18    val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
   20.19   in hd (Variable.export ctxt' ctxt [th13])
   20.20   end
    21.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 09 15:14:21 2011 +0200
    21.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 09 23:30:18 2011 +0200
    21.3 @@ -622,7 +622,7 @@
    21.4                (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
    21.5          let
    21.6            val permT = mk_permT
    21.7 -            (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
    21.8 +            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
    21.9            val pi = Free ("pi", permT);
   21.10            val T = Type (Sign.intern_type thy name, map TFree tvs);
   21.11          in apfst (pair r o hd)
   21.12 @@ -1169,7 +1169,7 @@
   21.13          val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   21.14          val frees = tnames ~~ Ts;
   21.15          val frees' = partition_cargs idxs frees;
   21.16 -        val z = (Name.variant tnames "z", fsT);
   21.17 +        val z = (singleton (Name.variant_list tnames) "z", fsT);
   21.18  
   21.19          fun mk_prem ((dt, s), T) =
   21.20            let
    22.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 09 15:14:21 2011 +0200
    22.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 09 23:30:18 2011 +0200
    22.3 @@ -200,7 +200,7 @@
    22.4      val ind_sort = if null atomTs then HOLogic.typeS
    22.5        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
    22.6          ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
    22.7 -    val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    22.8 +    val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
    22.9      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
   22.10      val fsT = TFree (fs_ctxt_tyname, ind_sort);
   22.11  
    23.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jun 09 15:14:21 2011 +0200
    23.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jun 09 23:30:18 2011 +0200
    23.3 @@ -226,7 +226,7 @@
    23.4      val ind_sort = if null atomTs then HOLogic.typeS
    23.5        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
    23.6          ("fs_" ^ Long_Name.base_name a)) atoms));
    23.7 -    val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    23.8 +    val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
    23.9      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
   23.10      val fsT = TFree (fs_ctxt_tyname, ind_sort);
   23.11  
    24.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 15:14:21 2011 +0200
    24.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 23:30:18 2011 +0200
    24.3 @@ -36,7 +36,7 @@
    24.4    let
    24.5      val (vs, Ts) = split_list (strip_qnt_vars "all" t);
    24.6      val body = strip_qnt_body "all" t;
    24.7 -    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
    24.8 +    val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
    24.9        (fn Free (v, _) => insert (op =) v | _ => I) body []))
   24.10    in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
   24.11  
   24.12 @@ -207,7 +207,7 @@
   24.13  fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
   24.14    let
   24.15      val used = map fst (fold Term.add_frees fs []);
   24.16 -    val x = (Name.variant used "x", dummyT);
   24.17 +    val x = (singleton (Name.variant_list used) "x", dummyT);
   24.18      val frees = ls @ x :: rs;
   24.19      val raw_rhs = list_abs_free (frees,
   24.20        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
    25.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 09 15:14:21 2011 +0200
    25.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 09 23:30:18 2011 +0200
    25.3 @@ -136,7 +136,7 @@
    25.4  fun mk_variables thy prfx xs ty (tab, ctxt) =
    25.5    let
    25.6      val T = mk_type thy prfx ty;
    25.7 -    val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
    25.8 +    val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
    25.9      val zs = map (Free o rpair T) ys;
   25.10    in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
   25.11  
   25.12 @@ -779,7 +779,7 @@
   25.13        map_filter (fn s => lookup funs s |>
   25.14          Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
   25.15        split_list ||> split_list;
   25.16 -    val (fs', ctxt') = Name.variants fs ctxt
   25.17 +    val (fs', ctxt') = fold_map Name.variant fs ctxt
   25.18    in
   25.19      (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
   25.20       Element.Fixes (map2 (fn s => fn T =>
    26.1 --- a/src/HOL/Statespace/state_space.ML	Thu Jun 09 15:14:21 2011 +0200
    26.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Jun 09 23:30:18 2011 +0200
    26.3 @@ -379,8 +379,8 @@
    26.4  
    26.5      val Ts = distinct_types (map snd all_comps);
    26.6      val arg_names = map fst args;
    26.7 -    val valueN = Name.variant arg_names "'value";
    26.8 -    val nameN = Name.variant (valueN::arg_names) "'name";
    26.9 +    val valueN = singleton (Name.variant_list arg_names) "'value";
   26.10 +    val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
   26.11      val valueT = TFree (valueN, Sign.defaultS thy);
   26.12      val nameT = TFree (nameN, Sign.defaultS thy);
   26.13      val stateT = nameT --> valueT;
    27.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 15:14:21 2011 +0200
    27.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 23:30:18 2011 +0200
    27.3 @@ -849,7 +849,7 @@
    27.4        |>> (introduce_proxies format type_sys #> AAtom)
    27.5        ||> union (op =) atomic_types
    27.6      fun do_quant bs q s T t' =
    27.7 -      let val s = Name.variant (map fst bs) s in
    27.8 +      let val s = singleton (Name.variant_list (map fst bs)) s in
    27.9          do_formula ((s, T) :: bs) t'
   27.10          #>> mk_aquant q [(`make_bound_var s, SOME T)]
   27.11        end
    28.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jun 09 15:14:21 2011 +0200
    28.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jun 09 23:30:18 2011 +0200
    28.3 @@ -281,7 +281,7 @@
    28.4      val recTs = Datatype_Aux.get_rec_types descr' sorts;
    28.5      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    28.6      val newTs = take (length (hd descr)) recTs;
    28.7 -    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    28.8 +    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
    28.9  
   28.10      fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
   28.11  
    29.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jun 09 15:14:21 2011 +0200
    29.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jun 09 23:30:18 2011 +0200
    29.3 @@ -152,7 +152,7 @@
    29.4   
    29.5  fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
    29.6    let
    29.7 -    val name = Name.variant used "a";
    29.8 +    val name = singleton (Name.variant_list used) "a";
    29.9      fun expand constructors used ty ((_, []), _) =
   29.10            raise CASE_ERROR ("mk_case: expand_var_row", ~1)
   29.11        | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
   29.12 @@ -264,11 +264,12 @@
   29.13  
   29.14          (* replace occurrences of dummy_pattern by distinct variables *)
   29.15          (* internalize constant names                                 *)
   29.16 +        (* FIXME proper name context!? *)
   29.17          fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
   29.18                let val (t', used') = prep_pat t used
   29.19                in (c $ t' $ tT, used') end
   29.20            | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
   29.21 -              let val x = Name.variant used "x"
   29.22 +              let val x = singleton (Name.variant_list used) "x"
   29.23                in (Free (x, T), x :: used) end
   29.24            | prep_pat (Const (s, T)) used =
   29.25                (Const (intern_const_syntax s, T), used)
   29.26 @@ -305,6 +306,7 @@
   29.27  
   29.28  (* destruct one level of pattern matching *)
   29.29  
   29.30 +(* FIXME proper name context!? *)
   29.31  fun gen_dest_case name_of type_of tab d used t =
   29.32    (case apfst name_of (strip_comb t) of
   29.33      (SOME cname, ts as _ :: _) =>
   29.34 @@ -345,7 +347,7 @@
   29.35                  val R = type_of t;
   29.36                  val dummy =
   29.37                    if d then Const (@{const_name dummy_pattern}, R)
   29.38 -                  else Free (Name.variant used "x", R);
   29.39 +                  else Free (singleton (Name.variant_list used) "x", R);
   29.40                in
   29.41                  SOME (x,
   29.42                    map mk_case
    30.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Jun 09 15:14:21 2011 +0200
    30.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Jun 09 23:30:18 2011 +0200
    30.3 @@ -47,7 +47,7 @@
    30.4        |> Term.strip_comb
    30.5        |> apsnd (fst o split_last)
    30.6        |> list_comb;
    30.7 -    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
    30.8 +    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    30.9      val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   30.10    in
   30.11      thms
    31.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jun 09 15:14:21 2011 +0200
    31.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jun 09 23:30:18 2011 +0200
    31.3 @@ -134,7 +134,7 @@
    31.4  
    31.5      val names = map Long_Name.base_name (the_default tycos (#alt_names info));
    31.6      val (auxnames, _) = Name.make_context names
    31.7 -      |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
    31.8 +      |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
    31.9      val prefix = space_implode "_" names;
   31.10  
   31.11    in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
   31.12 @@ -407,7 +407,7 @@
   31.13      fun inter_sort m = map (fn xs => nth xs m) raw_vss
   31.14        |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   31.15      val sorts = map inter_sort ms;
   31.16 -    val vs = Name.names Name.context Name.aT sorts;
   31.17 +    val vs = Name.invent_names Name.context Name.aT sorts;
   31.18  
   31.19      fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
   31.20        (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
    32.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Jun 09 15:14:21 2011 +0200
    32.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Jun 09 23:30:18 2011 +0200
    32.3 @@ -263,7 +263,7 @@
    32.4      val recTs = Datatype_Aux.get_rec_types descr' sorts;
    32.5      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    32.6      val newTs = take (length (hd descr)) recTs;
    32.7 -    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    32.8 +    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
    32.9  
   32.10      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   32.11        map (fn (_, cargs) =>
   32.12 @@ -310,7 +310,7 @@
   32.13      val recTs = Datatype_Aux.get_rec_types descr' sorts;
   32.14      val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   32.15      val newTs = take (length (hd descr)) recTs;
   32.16 -    val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   32.17 +    val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
   32.18      val P = Free ("P", T' --> HOLogic.boolT);
   32.19  
   32.20      fun make_split (((_, (_, _, constrs)), T), comb_t) =
    33.1 --- a/src/HOL/Tools/Function/fun.ML	Thu Jun 09 15:14:21 2011 +0200
    33.2 +++ b/src/HOL/Tools/Function/fun.ML	Thu Jun 09 23:30:18 2011 +0200
    33.3 @@ -64,7 +64,7 @@
    33.4          val (argTs, rT) = chop n (binder_types fT)
    33.5            |> apsnd (fn Ts => Ts ---> body_type fT)
    33.6  
    33.7 -        val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
    33.8 +        val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
    33.9        in
   33.10          HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
   33.11            Const ("HOL.undefined", rT))
    34.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 15:14:21 2011 +0200
    34.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 23:30:18 2011 +0200
    34.3 @@ -75,7 +75,7 @@
    34.4          in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    34.5        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    34.6          (*Universal quant: insert a free variable into body and continue*)
    34.7 -        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    34.8 +        let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
    34.9          in dec_sko (subst_bound (Free(fname,T), p)) rhss end
   34.10        | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
   34.11        | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    35.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 15:14:21 2011 +0200
    35.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 23:30:18 2011 +0200
    35.3 @@ -167,12 +167,19 @@
    35.4  
    35.5  (* INFERENCE RULE: RESOLVE *)
    35.6  
    35.7 +(*Increment the indexes of only the type variables*)
    35.8 +fun incr_type_indexes inc th =
    35.9 +  let val tvs = Term.add_tvars (Thm.full_prop_of th) []
   35.10 +      and thy = Thm.theory_of_thm th
   35.11 +      fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
   35.12 +  in Thm.instantiate (map inc_tvar tvs, []) th end;
   35.13 +
   35.14  (* Like RSN, but we rename apart only the type variables. Vars here typically
   35.15     have an index of 1, and the use of RSN would increase this typically to 3.
   35.16     Instantiations of those Vars could then fail. *)
   35.17  fun resolve_inc_tyvars thy tha i thb =
   35.18    let
   35.19 -    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   35.20 +    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
   35.21      fun aux tha thb =
   35.22        case Thm.bicompose false (false, tha, nprems_of tha) i thb
   35.23             |> Seq.list_of |> distinct Thm.eq_thm of
   35.24 @@ -199,7 +206,7 @@
   35.25                     |> map (fn (x, (S, T)) =>
   35.26                                pairself (ctyp_of thy) (TVar (x, S), T)) of
   35.27               [] => raise TERM z
   35.28 -           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
   35.29 +           | ps => aux (Drule.instantiate_normalize (ps, []) tha) (Drule.instantiate_normalize (ps, []) thb)
   35.30    end
   35.31  
   35.32  fun s_not (@{const Not} $ t) = t
   35.33 @@ -555,7 +562,7 @@
   35.34                          tyenv []
   35.35            val t_inst =
   35.36              [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
   35.37 -        in th |> instantiate (ty_inst, t_inst) end
   35.38 +        in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
   35.39        | _ => raise Fail "expected a single non-zapped, non-Metis Var"
   35.40    in
   35.41      (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
    36.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jun 09 15:14:21 2011 +0200
    36.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jun 09 23:30:18 2011 +0200
    36.3 @@ -205,7 +205,7 @@
    36.4        (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
    36.5          (Symbol.explode name)))
    36.6      val name'' = f (if name' = "" then empty else name')
    36.7 -  in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
    36.8 +  in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
    36.9  
   36.10  (** constant table **)
   36.11  
    37.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Jun 09 15:14:21 2011 +0200
    37.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Jun 09 23:30:18 2011 +0200
    37.3 @@ -249,7 +249,7 @@
    37.4            end
    37.5          else
    37.6            let
    37.7 -            val s = Name.variant names "x"
    37.8 +            val s = singleton (Name.variant_list names) "x"
    37.9              val v = Free (s, fastype_of t)
   37.10            in
   37.11              (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
   37.12 @@ -257,7 +257,7 @@
   37.13  (*
   37.14    if is_constrt thy t then (t, (names, eqs)) else
   37.15      let
   37.16 -      val s = Name.variant names "x"
   37.17 +      val s = singleton (Name.variant_list names) "x"
   37.18        val v = Free (s, fastype_of t)
   37.19      in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
   37.20  *)
    38.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 15:14:21 2011 +0200
    38.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 23:30:18 2011 +0200
    38.3 @@ -542,7 +542,7 @@
    38.4  fun focus_ex t nctxt =
    38.5    let
    38.6      val ((xs, Ts), t') = apfst split_list (strip_ex t) 
    38.7 -    val (xs', nctxt') = Name.variants xs nctxt;
    38.8 +    val (xs', nctxt') = fold_map Name.variant xs nctxt;
    38.9      val ps' = xs' ~~ Ts;
   38.10      val vs = map Free ps';
   38.11      val t'' = Term.subst_bounds (rev vs, t');
   38.12 @@ -906,7 +906,7 @@
   38.13          val Type ("fun", [T, T']) = fastype_of comb;
   38.14          val (Const (case_name, _), fs) = strip_comb comb
   38.15          val used = Term.add_tfree_names comb []
   38.16 -        val U = TFree (Name.variant used "'t", HOLogic.typeS)
   38.17 +        val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
   38.18          val x = Free ("x", T)
   38.19          val f = Free ("f", T' --> U)
   38.20          fun apply_f f' =
    39.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 09 15:14:21 2011 +0200
    39.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 09 23:30:18 2011 +0200
    39.3 @@ -302,7 +302,7 @@
    39.4    mk_random = (fn _ => error "no random generation"),
    39.5    additional_arguments = fn names =>
    39.6      let
    39.7 -      val depth_name = Name.variant names "depth"
    39.8 +      val depth_name = singleton (Name.variant_list names) "depth"
    39.9      in [Free (depth_name, @{typ code_numeral})] end,
   39.10    modify_funT = (fn T => let val (Ts, U) = strip_type T
   39.11    val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
   39.12 @@ -563,7 +563,7 @@
   39.13        NONE => (Free (s, T), (names, (s, [])::vs))
   39.14      | SOME xs =>
   39.15          let
   39.16 -          val s' = Name.variant names s;
   39.17 +          val s' = singleton (Name.variant_list names) s;
   39.18            val v = Free (s', T)
   39.19          in
   39.20            (v, (s'::names, AList.update (op =) (s, v::xs) vs))
   39.21 @@ -626,8 +626,8 @@
   39.22      val eqs'' =
   39.23        map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
   39.24      val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
   39.25 -    val name = Name.variant names "x";
   39.26 -    val name' = Name.variant (name :: names) "y";
   39.27 +    val name = singleton (Name.variant_list names) "x";
   39.28 +    val name' = singleton (Name.variant_list (name :: names)) "y";
   39.29      val T = HOLogic.mk_tupleT (map fastype_of out_ts);
   39.30      val U = fastype_of success_t;
   39.31      val U' = dest_predT compfuns U;
   39.32 @@ -905,7 +905,7 @@
   39.33        let
   39.34          val (i, is) = argument_position_of mode position
   39.35          val inp_var = nth_pair is (nth in_ts' i)
   39.36 -        val x = Name.variant all_vs "x"
   39.37 +        val x = singleton (Name.variant_list all_vs) "x"
   39.38          val xt = Free (x, fastype_of inp_var)
   39.39          fun compile_single_case ((c, T), switched) =
   39.40            let
   39.41 @@ -962,7 +962,7 @@
   39.42            (Free (hd param_vs, T), (tl param_vs, names))
   39.43          else
   39.44            let
   39.45 -            val new = Name.variant names "x"
   39.46 +            val new = singleton (Name.variant_list names) "x"
   39.47            in (Free (new, T), (param_vs, new :: names)) end)) inpTs
   39.48          (param_vs, (all_vs @ param_vs))
   39.49      val in_ts' = map_filter (map_filter_prod
   39.50 @@ -1009,7 +1009,7 @@
   39.51  fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
   39.52      if eq_mode (m, Input) orelse eq_mode (m, Output) then
   39.53        let
   39.54 -        val x = Name.variant names "x"
   39.55 +        val x = singleton (Name.variant_list names) "x"
   39.56        in
   39.57          (Free (x, T), x :: names)
   39.58        end
   39.59 @@ -1023,7 +1023,7 @@
   39.60    | mk_args is_eval ((m as Fun _), T) names =
   39.61      let
   39.62        val funT = funT_of PredicateCompFuns.compfuns m T
   39.63 -      val x = Name.variant names "x"
   39.64 +      val x = singleton (Name.variant_list names) "x"
   39.65        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
   39.66        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
   39.67        val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
   39.68 @@ -1033,7 +1033,7 @@
   39.69      end
   39.70    | mk_args is_eval (_, T) names =
   39.71      let
   39.72 -      val x = Name.variant names "x"
   39.73 +      val x = singleton (Name.variant_list names) "x"
   39.74      in
   39.75        (Free (x, T), x :: names)
   39.76      end
    40.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jun 09 15:14:21 2011 +0200
    40.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jun 09 23:30:18 2011 +0200
    40.3 @@ -129,7 +129,7 @@
    40.4  
    40.5  fun declare_names s xs ctxt =
    40.6    let
    40.7 -    val res = Name.names ctxt s xs
    40.8 +    val res = Name.invent_names ctxt s xs
    40.9    in (res, fold Name.declare (map fst res) ctxt) end
   40.10    
   40.11  fun split_all_pairs thy th =
    41.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 15:14:21 2011 +0200
    41.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 23:30:18 2011 +0200
    41.3 @@ -84,8 +84,8 @@
    41.4      val (argTs, resT) = strip_type (fastype_of func)
    41.5      val nctxt =
    41.6        Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
    41.7 -    val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
    41.8 -    val ([resname], nctxt'') = Name.variants ["r"] nctxt'
    41.9 +    val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
   41.10 +    val (resname, nctxt'') = Name.variant "r" nctxt'
   41.11      val args = map Free (argnames ~~ argTs)
   41.12      val res = Free (resname, resT)
   41.13    in Logic.mk_equals
   41.14 @@ -118,7 +118,7 @@
   41.15            val absnames = Name.variant_list names (map fst vars)
   41.16            val frees = map2 (curry Free) absnames (map snd vars)
   41.17            val body' = subst_bounds (rev frees, body)
   41.18 -          val resname = Name.variant (absnames @ names) "res"
   41.19 +          val resname = singleton (Name.variant_list (absnames @ names)) "res"
   41.20            val resvar = Free (resname, fastype_of body)
   41.21            val t = flatten' body' ([], [])
   41.22              |> map (fn (res, (inner_names, inner_prems)) =>
   41.23 @@ -241,7 +241,7 @@
   41.24                              HOLogic.mk_eq (@{term False}, Bound 0)))
   41.25                          end
   41.26                      val argvs' = map2 lift_arg Ts argvs
   41.27 -                    val resname = Name.variant names' "res"
   41.28 +                    val resname = singleton (Name.variant_list names') "res"
   41.29                      val resvar = Free (resname, body_type (fastype_of t))
   41.30                      val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
   41.31                    in (resvar, (resname :: names', prem :: prems')) end))
    42.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jun 09 15:14:21 2011 +0200
    42.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jun 09 23:30:18 2011 +0200
    42.3 @@ -77,7 +77,7 @@
    42.4    if is_compound atom then
    42.5      let
    42.6        val atom = Envir.beta_norm (Pattern.eta_long [] atom)
    42.7 -      val constname = Name.variant (map (Long_Name.base_name o fst) defs)
    42.8 +      val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
    42.9          ((Long_Name.base_name constname) ^ "_aux")
   42.10        val full_constname = Sign.full_bname thy constname
   42.11        val (params, args) = List.partition (is_predT o fastype_of)
   42.12 @@ -108,7 +108,7 @@
   42.13        | SOME (atom', srs) =>
   42.14          let      
   42.15            val frees = map Free (Term.add_frees atom' [])
   42.16 -          val constname = Name.variant (map (Long_Name.base_name o fst) defs)
   42.17 +          val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
   42.18             ((Long_Name.base_name constname) ^ "_aux")
   42.19            val full_constname = Sign.full_bname thy constname
   42.20            val constT = map fastype_of frees ---> HOLogic.boolT
   42.21 @@ -239,8 +239,9 @@
   42.22              val vars = map Var (Term.add_vars abs_arg [])
   42.23              val abs_arg' = Logic.unvarify_global abs_arg
   42.24              val frees = map Free (Term.add_frees abs_arg' [])
   42.25 -            val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
   42.26 -              ((Long_Name.base_name constname) ^ "_hoaux")
   42.27 +            val constname =
   42.28 +              singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
   42.29 +                ((Long_Name.base_name constname) ^ "_hoaux")
   42.30              val full_constname = Sign.full_bname thy constname
   42.31              val constT = map fastype_of frees ---> (fastype_of abs_arg')
   42.32              val const = Const (full_constname, constT)
    43.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Jun 09 15:14:21 2011 +0200
    43.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Jun 09 23:30:18 2011 +0200
    43.3 @@ -73,7 +73,8 @@
    43.4      fun mk_fresh_name names =
    43.5        let
    43.6          val name =
    43.7 -          Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
    43.8 +          singleton (Name.variant_list names)
    43.9 +            ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
   43.10          val bname = Sign.full_bname thy name
   43.11        in
   43.12          if Sign.declared_const thy bname then
   43.13 @@ -119,7 +120,7 @@
   43.14      val add_vars = fold_aterms (fn Var v => cons v | _ => I);
   43.15      fun fresh_free T free_names =
   43.16        let
   43.17 -        val free_name = Name.variant free_names "x"
   43.18 +        val free_name = singleton (Name.variant_list free_names) "x"
   43.19        in
   43.20          (Free (free_name, T), free_name :: free_names)
   43.21        end
    44.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Jun 09 15:14:21 2011 +0200
    44.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Jun 09 23:30:18 2011 +0200
    44.3 @@ -156,10 +156,10 @@
    44.4        [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
    44.5    let
    44.6     val (mp', mq') = (get_pmi th_1, get_pmi th_1')
    44.7 -   val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
    44.8 +   val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
    44.9                     [th_1, th_1']
   44.10 -   val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
   44.11 -   val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
   44.12 +   val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
   44.13 +   val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
   44.14    in (mi_th, set_th, infD_th)
   44.15    end;
   44.16  
    45.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 15:14:21 2011 +0200
    45.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 23:30:18 2011 +0200
    45.3 @@ -67,7 +67,7 @@
    45.4  
    45.5  fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
    45.6    let
    45.7 -    val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
    45.8 +    val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
    45.9      val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
   45.10        $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
   45.11      val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    46.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 09 15:14:21 2011 +0200
    46.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 09 23:30:18 2011 +0200
    46.3 @@ -100,7 +100,7 @@
    46.4      val cT_random_aux = inst pt_random_aux;
    46.5      val cT_rhs = inst pt_rhs;
    46.6      val rule = @{thm random_aux_rec}
    46.7 -      |> Drule.instantiate ([(aT, icT)],
    46.8 +      |> Drule.instantiate_normalize ([(aT, icT)],
    46.9             [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
   46.10      val tac = ALLGOALS (rtac rule)
   46.11        THEN ALLGOALS (simp_tac rew_ss)
   46.12 @@ -214,7 +214,7 @@
   46.13          val tTs = (map o apsnd) termifyT simple_tTs;
   46.14          val is_rec = exists is_some ks;
   46.15          val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
   46.16 -        val vs = Name.names Name.context "x" (map snd simple_tTs);
   46.17 +        val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
   46.18          val tc = HOLogic.mk_return T @{typ Random.seed}
   46.19            (HOLogic.mk_valtermify_app c vs simpleT);
   46.20          val t = HOLogic.mk_ST
    47.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jun 09 15:14:21 2011 +0200
    47.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jun 09 23:30:18 2011 +0200
    47.3 @@ -108,7 +108,7 @@
    47.4      | SOME thm' =>
    47.5          (case try (get_match_inst thy (get_lhs thm')) redex of
    47.6            NONE => NONE
    47.7 -        | SOME inst2 => try (Drule.instantiate inst2) thm'))
    47.8 +        | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
    47.9    end
   47.10  
   47.11  fun ball_bex_range_simproc ss redex =
   47.12 @@ -490,7 +490,7 @@
   47.13            if ty_c = ty_d
   47.14            then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   47.15            else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   47.16 -        val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
   47.17 +        val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
   47.18        in
   47.19          Conv.rewr_conv thm4 ctrm
   47.20        end
    48.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 15:14:21 2011 +0200
    48.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 23:30:18 2011 +0200
    48.3 @@ -155,7 +155,7 @@
    48.4  fun close_form t =
    48.5    (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
    48.6    |> fold (fn ((s, i), T) => fn (t', taken) =>
    48.7 -              let val s' = Name.variant taken s in
    48.8 +              let val s' = singleton (Name.variant_list taken) s in
    48.9                  ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   48.10                    else Term.all) T
   48.11                   $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
    49.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Jun 09 15:14:21 2011 +0200
    49.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Jun 09 23:30:18 2011 +0200
    49.3 @@ -270,7 +270,7 @@
    49.4        val gspec = Thm.forall_intr (cterm_of thy x) spec
    49.5  in
    49.6  fun SPEC tm thm =
    49.7 -   let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
    49.8 +   let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_term tm)], []) gspec
    49.9     in thm RS (Thm.forall_elim tm gspec') end
   49.10  end;
   49.11  
   49.12 @@ -298,7 +298,7 @@
   49.13         val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
   49.14         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   49.15         val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
   49.16 -       val allI2 = instantiate (certify thy theta) allI
   49.17 +       val allI2 = Drule.instantiate_normalize (certify thy theta) allI
   49.18         val thm = Thm.implies_elim allI2 gth
   49.19         val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
   49.20         val prop' = tp $ (A $ Abs(x,ty,M))
    50.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Jun 09 15:14:21 2011 +0200
    50.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Jun 09 23:30:18 2011 +0200
    50.3 @@ -324,7 +324,7 @@
    50.4                                map_index (fn (i, t) => (t,(i,true))) R)
    50.5       val names = List.foldr OldTerm.add_term_names [] R
    50.6       val atype = type_of(hd pats)
    50.7 -     and aname = Name.variant names "a"
    50.8 +     and aname = singleton (Name.variant_list names) "a"
    50.9       val a = Free(aname,atype)
   50.10       val ty_info = Thry.match_info thy
   50.11       val ty_match = Thry.match_type thy
   50.12 @@ -480,7 +480,7 @@
   50.13       val tych = Thry.typecheck thy
   50.14       val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
   50.15       val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   50.16 -     val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
   50.17 +     val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
   50.18                     Rtype)
   50.19       val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
   50.20       val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
   50.21 @@ -679,8 +679,8 @@
   50.22   in fn pats =>
   50.23   let val names = List.foldr OldTerm.add_term_names [] pats
   50.24       val T = type_of (hd pats)
   50.25 -     val aname = Name.variant names "a"
   50.26 -     val vname = Name.variant (aname::names) "v"
   50.27 +     val aname = singleton (Name.variant_list names) "a"
   50.28 +     val vname = singleton (Name.variant_list (aname::names)) "v"
   50.29       val a = Free (aname, T)
   50.30       val v = Free (vname, T)
   50.31       val a_eq_v = HOLogic.mk_eq(a,v)
   50.32 @@ -830,8 +830,8 @@
   50.33      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   50.34      val case_thm = complete_cases thy pats
   50.35      val domain = (type_of o hd) pats
   50.36 -    val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
   50.37 -                              [] (pats::TCsl)) "P"
   50.38 +    val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
   50.39 +                              [] (pats::TCsl))) "P"
   50.40      val P = Free(Pname, domain --> HOLogic.boolT)
   50.41      val Sinduct = Rules.SPEC (tych P) Sinduction
   50.42      val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
   50.43 @@ -841,9 +841,10 @@
   50.44      val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
   50.45      val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
   50.46      val proved_cases = map (prove_case fconst thy) tasks
   50.47 -    val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
   50.48 -                    "v",
   50.49 -                  domain)
   50.50 +    val v =
   50.51 +      Free (singleton
   50.52 +        (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
   50.53 +          domain)
   50.54      val vtyped = tych v
   50.55      val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   50.56      val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
    51.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 09 15:14:21 2011 +0200
    51.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 09 23:30:18 2011 +0200
    51.3 @@ -238,7 +238,7 @@
    51.4  
    51.5  fun dest_abs used (a as Abs(s, ty, M)) =
    51.6       let
    51.7 -       val s' = Name.variant used s;
    51.8 +       val s' = singleton (Name.variant_list used) s;
    51.9         val v = Free(s', ty);
   51.10       in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
   51.11       end
    52.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu Jun 09 15:14:21 2011 +0200
    52.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu Jun 09 23:30:18 2011 +0200
    52.3 @@ -57,7 +57,7 @@
    52.4  fun mk_term_of_eq thy ty (c, (_, tys)) =
    52.5    let
    52.6      val t = list_comb (Const (c, tys ---> ty),
    52.7 -      map Free (Name.names Name.context "a" tys));
    52.8 +      map Free (Name.invent_names Name.context "a" tys));
    52.9      val (arg, rhs) =
   52.10        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
   52.11          (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    53.1 --- a/src/HOL/Tools/enriched_type.ML	Thu Jun 09 15:14:21 2011 +0200
    53.2 +++ b/src/HOL/Tools/enriched_type.ML	Thu Jun 09 23:30:18 2011 +0200
    53.3 @@ -98,7 +98,7 @@
    53.4      val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
    53.5      fun invents n k nctxt =
    53.6        let
    53.7 -        val names = Name.invents nctxt n k;
    53.8 +        val names = Name.invent nctxt n k;
    53.9        in (names, fold Name.declare names nctxt) end;
   53.10      val ((names21, names32), nctxt) = Variable.names_of ctxt
   53.11        |> invents "f" (length Ts21)
   53.12 @@ -120,7 +120,7 @@
   53.13      val mapper31 = mk_mapper T3 T1 args31;
   53.14      val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   53.15        (HOLogic.mk_comp (mapper21, mapper32), mapper31);
   53.16 -    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
   53.17 +    val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
   53.18      val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   53.19        (mapper21 $ (mapper32 $ x), mapper31 $ x);
   53.20      val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
    54.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 15:14:21 2011 +0200
    54.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 23:30:18 2011 +0200
    54.3 @@ -326,7 +326,7 @@
    54.4    (case AList.lookup (op =) vs s of
    54.5      NONE => (s, (names, (s, [s])::vs))
    54.6    | SOME xs =>
    54.7 -      let val s' = Name.variant names s
    54.8 +      let val s' = singleton (Name.variant_list names) s
    54.9        in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
   54.10  
   54.11  fun distinct_v (Var ((s, 0), T)) nvs =
   54.12 @@ -414,7 +414,7 @@
   54.13      fun check_constrt t (names, eqs) =
   54.14        if is_constrt thy t then (t, (names, eqs))
   54.15        else
   54.16 -        let val s = Name.variant names "x";
   54.17 +        let val s = singleton (Name.variant_list names) "x";
   54.18          in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
   54.19  
   54.20      fun compile_eq (s, t) gr =
    55.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 15:14:21 2011 +0200
    55.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 23:30:18 2011 +0200
    55.3 @@ -36,7 +36,7 @@
    55.4  
    55.5  fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
    55.6        let val (s', names') = (case names of
    55.7 -          [] => (Name.variant used s, [])
    55.8 +          [] => (singleton (Name.variant_list used) s, [])
    55.9          | name :: names' => (name, names'))
   55.10        in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   55.11    | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
   55.12 @@ -246,7 +246,7 @@
   55.13      handle Datatype_Aux.Datatype_Empty name' =>
   55.14        let
   55.15          val name = Long_Name.base_name name';
   55.16 -        val dname = Name.variant used "Dummy";
   55.17 +        val dname = singleton (Name.variant_list used) "Dummy";
   55.18        in
   55.19          thy
   55.20          |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
    56.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Jun 09 15:14:21 2011 +0200
    56.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Jun 09 23:30:18 2011 +0200
    56.3 @@ -63,9 +63,9 @@
    56.4    let
    56.5      val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
    56.6      and ct = cterm_of thy t
    56.7 -  in instantiate ([], [(cn, ct)]) @{thm le0} end;
    56.8 +  in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
    56.9  
   56.10 -end;  (* LA_Logic *)
   56.11 +end;
   56.12  
   56.13  
   56.14  (* arith context data *)
    57.1 --- a/src/HOL/Tools/primrec.ML	Thu Jun 09 15:14:21 2011 +0200
    57.2 +++ b/src/HOL/Tools/primrec.ML	Thu Jun 09 23:30:18 2011 +0200
    57.3 @@ -38,7 +38,7 @@
    57.4    let
    57.5      val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
    57.6      val body = strip_qnt_body "all" spec;
    57.7 -    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
    57.8 +    val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
    57.9        (fn Free (v, _) => insert (op =) v | _ => I) body []));
   57.10      val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
   57.11      val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)
    58.1 --- a/src/HOL/Tools/record.ML	Thu Jun 09 15:14:21 2011 +0200
    58.2 +++ b/src/HOL/Tools/record.ML	Thu Jun 09 23:30:18 2011 +0200
    58.3 @@ -1662,7 +1662,7 @@
    58.4      val variants = map (fn Free (x, _) => x) vars_more;
    58.5      val ext = mk_ext vars_more;
    58.6      val s = Free (rN, extT);
    58.7 -    val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
    58.8 +    val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
    58.9  
   58.10      val inject_prop =
   58.11        let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
   58.12 @@ -1677,7 +1677,7 @@
   58.13        (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
   58.14  
   58.15      val split_meta_prop =
   58.16 -      let val P = Free (Name.variant variants "P", extT --> Term.propT) in
   58.17 +      let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
   58.18          Logic.mk_equals
   58.19           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
   58.20        end;
   58.21 @@ -1801,7 +1801,7 @@
   58.22      fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
   58.23      val T = Type (tyco, map TFree vs);
   58.24      val Tm = termifyT T;
   58.25 -    val params = Name.names Name.context "x" Ts;
   58.26 +    val params = Name.invent_names Name.context "x" Ts;
   58.27      val lhs = HOLogic.mk_random T size;
   58.28      val tc = HOLogic.mk_return Tm @{typ Random.seed}
   58.29        (HOLogic.mk_valtermify_app extN params T);
   58.30 @@ -1820,7 +1820,7 @@
   58.31      fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
   58.32      val T = Type (tyco, map TFree vs);
   58.33      val test_function = Free ("f", termifyT T --> @{typ "term list option"});
   58.34 -    val params = Name.names Name.context "x" Ts;
   58.35 +    val params = Name.invent_names Name.context "x" Ts;
   58.36      fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   58.37        --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
   58.38      fun mk_full_exhaustive T =
   58.39 @@ -1938,7 +1938,7 @@
   58.40      val all_vars = parent_vars @ vars;
   58.41      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
   58.42  
   58.43 -    val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
   58.44 +    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
   58.45      val moreT = TFree zeta;
   58.46      val more = Free (moreN, moreT);
   58.47      val full_moreN = full (Binding.name moreN);
   58.48 @@ -2134,9 +2134,9 @@
   58.49  
   58.50      (* prepare propositions *)
   58.51      val _ = timing_msg "record preparing propositions";
   58.52 -    val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
   58.53 -    val C = Free (Name.variant all_variants "C", HOLogic.boolT);
   58.54 -    val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
   58.55 +    val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
   58.56 +    val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
   58.57 +    val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
   58.58  
   58.59      (*selectors*)
   58.60      val sel_conv_props =
   58.61 @@ -2145,7 +2145,8 @@
   58.62      (*updates*)
   58.63      fun mk_upd_prop i (c, T) =
   58.64        let
   58.65 -        val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
   58.66 +        val x' =
   58.67 +          Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
   58.68          val n = parent_fields_len + i;
   58.69          val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
   58.70        in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
   58.71 @@ -2174,7 +2175,9 @@
   58.72  
   58.73      (*split*)
   58.74      val split_meta_prop =
   58.75 -      let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
   58.76 +      let
   58.77 +        val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
   58.78 +      in
   58.79          Logic.mk_equals
   58.80           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
   58.81        end;
    59.1 --- a/src/HOL/Tools/split_rule.ML	Thu Jun 09 15:14:21 2011 +0200
    59.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Jun 09 23:30:18 2011 +0200
    59.3 @@ -73,7 +73,7 @@
    59.4          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    59.5          val (vs', insts) = fold mk_tuple ts (vs, []);
    59.6        in
    59.7 -        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    59.8 +        (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    59.9        end
   59.10    | complete_split_rule_var _ x = x;
   59.11  
    60.1 --- a/src/HOL/Typerep.thy	Thu Jun 09 15:14:21 2011 +0200
    60.2 +++ b/src/HOL/Typerep.thy	Thu Jun 09 23:30:18 2011 +0200
    60.3 @@ -47,7 +47,7 @@
    60.4  fun add_typerep tyco thy =
    60.5    let
    60.6      val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
    60.7 -    val vs = Name.names Name.context "'a" sorts;
    60.8 +    val vs = Name.invent_names Name.context "'a" sorts;
    60.9      val ty = Type (tyco, map TFree vs);
   60.10      val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
   60.11        $ Free ("T", Term.itselfT ty);
    61.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jun 09 15:14:21 2011 +0200
    61.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jun 09 23:30:18 2011 +0200
    61.3 @@ -749,7 +749,7 @@
    61.4                      let
    61.5                        val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)
    61.6                        val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes
    61.7 -                        (Name.invents (Variable.names_of ctxt') Name.uu (length Ts - length params))
    61.8 +                        (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params))
    61.9                        val params' = (more_names @ param_names) ~~ Ts
   61.10                      in
   61.11                        trace_ex ctxt'' params' atoms (discr initems) n hist
    62.1 --- a/src/Provers/blast.ML	Thu Jun 09 15:14:21 2011 +0200
    62.2 +++ b/src/Provers/blast.ML	Thu Jun 09 23:30:18 2011 +0200
    62.3 @@ -1234,18 +1234,14 @@
    62.4    in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
    62.5  
    62.6  
    62.7 -(*Tactic using tableau engine and proof reconstruction.
    62.8 - "start" is CPU time at start, for printing SEARCH time
    62.9 -        (also prints reconstruction time)
   62.10 +(*Tableau engine and proof reconstruction operating on subgoal 1.
   62.11 + "start" is CPU time at start, for printing SEARCH time (also prints reconstruction time)
   62.12   "lim" is depth limit.*)
   62.13 -fun timing_depth_tac start ctxt lim i st0 =
   62.14 +fun raw_blast start ctxt lim st =
   62.15    let val thy = Proof_Context.theory_of ctxt
   62.16        val state = initialize ctxt
   62.17        val trace = Config.get ctxt trace;
   62.18        val stats = Config.get ctxt stats;
   62.19 -      val st = st0
   62.20 -        |> rotate_prems (i - 1)
   62.21 -        |> Conv.gconv_rule Object_Logic.atomize_prems 1
   62.22        val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
   62.23        val hyps  = strip_imp_prems skoprem
   62.24        and concl = strip_imp_concl skoprem
   62.25 @@ -1265,20 +1261,29 @@
   62.26            end
   62.27    in
   62.28      prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
   62.29 -    |> Seq.map (rotate_prems (1 - i))
   62.30    end
   62.31 -  handle PROVE => Seq.empty | THM _ => Seq.empty;
   62.32 +  handle PROVE => Seq.empty
   62.33 +    | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
   62.34  
   62.35 -(*Public version with fixed depth*)
   62.36 -fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
   62.37 +fun depth_tac ctxt lim i st =
   62.38 +  SELECT_GOAL
   62.39 +    (Object_Logic.atomize_prems_tac 1 THEN
   62.40 +      raw_blast (Timing.start ()) ctxt lim) i st;
   62.41 +
   62.42  
   62.43  val (depth_limit, setup_depth_limit) =
   62.44    Attrib.config_int @{binding blast_depth_limit} (K 20);
   62.45  
   62.46  fun blast_tac ctxt i st =
   62.47 -  ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i
   62.48 -    THEN flexflex_tac) st
   62.49 -  handle TRANS s => (if Config.get ctxt trace then warning ("blast: " ^ s) else (); Seq.empty);
   62.50 +  let
   62.51 +    val start = Timing.start ();
   62.52 +    val lim = Config.get ctxt depth_limit;
   62.53 +  in
   62.54 +    SELECT_GOAL
   62.55 +     (Object_Logic.atomize_prems_tac 1 THEN
   62.56 +      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN
   62.57 +      flexflex_tac) i st
   62.58 +  end;
   62.59  
   62.60  
   62.61  
    63.1 --- a/src/Provers/clasimp.ML	Thu Jun 09 15:14:21 2011 +0200
    63.2 +++ b/src/Provers/clasimp.ML	Thu Jun 09 23:30:18 2011 +0200
    63.3 @@ -117,10 +117,6 @@
    63.4  
    63.5  (* auto_tac *)
    63.6  
    63.7 -fun blast_depth_tac ctxt m i thm =
    63.8 -  Blast.depth_tac ctxt m i thm
    63.9 -    handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
   63.10 -
   63.11  (* a variant of depth_tac that avoids interference of the simplifier
   63.12     with dup_step_tac when they are combined by auto_tac *)
   63.13  local
   63.14 @@ -140,12 +136,12 @@
   63.15  
   63.16  end;
   63.17  
   63.18 -(*Designed to be idempotent, except if blast_depth_tac instantiates variables
   63.19 +(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
   63.20    in some of the subgoals*)
   63.21  fun mk_auto_tac ctxt m n =
   63.22    let
   63.23      val main_tac =
   63.24 -      blast_depth_tac ctxt m  (* fast but can't use wrappers *)
   63.25 +      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
   63.26        ORELSE'
   63.27        (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
   63.28    in
    64.1 --- a/src/Provers/hypsubst.ML	Thu Jun 09 15:14:21 2011 +0200
    64.2 +++ b/src/Provers/hypsubst.ML	Thu Jun 09 23:30:18 2011 +0200
    64.3 @@ -163,7 +163,7 @@
    64.4            | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
    64.5          val thy = Thm.theory_of_thm rl';
    64.6          val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
    64.7 -      in compose_tac (true, Drule.instantiate (instT,
    64.8 +      in compose_tac (true, Drule.instantiate_normalize (instT,
    64.9          map (pairself (cterm_of thy))
   64.10            [(Var (ixn, Ts ---> U --> body_type T), u),
   64.11             (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
    65.1 --- a/src/Pure/Isar/class.ML	Thu Jun 09 15:14:21 2011 +0200
    65.2 +++ b/src/Pure/Isar/class.ML	Thu Jun 09 23:30:18 2011 +0200
    65.3 @@ -426,7 +426,7 @@
    65.4        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    65.5      val tycos = map #1 all_arities;
    65.6      val (_, sorts, sort) = hd all_arities;
    65.7 -    val vs = Name.names Name.context Name.aT sorts;
    65.8 +    val vs = Name.invent_names Name.context Name.aT sorts;
    65.9    in (tycos, vs, sort) end;
   65.10  
   65.11  
    66.1 --- a/src/Pure/Isar/code.ML	Thu Jun 09 15:14:21 2011 +0200
    66.2 +++ b/src/Pure/Isar/code.ML	Thu Jun 09 23:30:18 2011 +0200
    66.3 @@ -433,7 +433,7 @@
    66.4        in (c, (vs'', binder_types ty')) end;
    66.5      val c' :: cs' = map (analyze_constructor thy) cs;
    66.6      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    66.7 -    val vs = Name.names Name.context Name.aT sorts;
    66.8 +    val vs = Name.invent_names Name.context Name.aT sorts;
    66.9      val cs''' = map (inst vs) cs'';
   66.10    in (tyco, (vs, rev cs''')) end;
   66.11  
   66.12 @@ -444,7 +444,7 @@
   66.13  fun get_type thy tyco = case get_type_entry thy tyco
   66.14   of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   66.15    | NONE => arity_number thy tyco
   66.16 -      |> Name.invents Name.context Name.aT
   66.17 +      |> Name.invent Name.context Name.aT
   66.18        |> map (rpair [])
   66.19        |> rpair []
   66.20        |> rpair false;
   66.21 @@ -779,7 +779,7 @@
   66.22          fun inter_sorts vs =
   66.23            fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
   66.24          val sorts = map_transpose inter_sorts vss;
   66.25 -        val vts = Name.names Name.context Name.aT sorts;
   66.26 +        val vts = Name.invent_names Name.context Name.aT sorts;
   66.27          val thms' =
   66.28            map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
   66.29          val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
   66.30 @@ -1145,8 +1145,8 @@
   66.31  
   66.32  fun case_cong thy case_const (num_args, (pos, _)) =
   66.33    let
   66.34 -    val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
   66.35 -    val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
   66.36 +    val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
   66.37 +    val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
   66.38      val (ws, vs) = chop pos zs;
   66.39      val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
   66.40      val Ts = binder_types T;
    67.1 --- a/src/Pure/Isar/obtain.ML	Thu Jun 09 15:14:21 2011 +0200
    67.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jun 09 23:30:18 2011 +0200
    67.3 @@ -133,7 +133,7 @@
    67.4      val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
    67.5  
    67.6      (*obtain statements*)
    67.7 -    val thesisN = Name.variant xs Auto_Bind.thesisN;
    67.8 +    val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
    67.9      val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
   67.10  
   67.11      val that_name = if name = "" then thatN else name;
    68.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Jun 09 15:14:21 2011 +0200
    68.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Jun 09 23:30:18 2011 +0200
    68.3 @@ -173,7 +173,7 @@
    68.4          else
    68.5            Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    68.6    in
    68.7 -    Drule.instantiate insts thm |> Rule_Cases.save thm
    68.8 +    Drule.instantiate_normalize insts thm |> Rule_Cases.save thm
    68.9    end;
   68.10  
   68.11  fun read_instantiate_mixed' ctxt (args, concl_args) thm =
   68.12 @@ -323,7 +323,7 @@
   68.13          fun liftpair (cv,ct) =
   68.14                (cterm_fun liftvar cv, cterm_fun liftterm ct)
   68.15          val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
   68.16 -        val rule = Drule.instantiate
   68.17 +        val rule = Drule.instantiate_normalize
   68.18                (map lifttvar envT', map liftpair cenv)
   68.19                (Thm.lift_rule (Thm.cprem_of st i) thm)
   68.20        in
   68.21 @@ -347,7 +347,7 @@
   68.22      val maxidx = Thm.maxidx_of rl;
   68.23      fun cvar xi = cert (Var (xi, propT));
   68.24      val revcut_rl' =
   68.25 -      instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   68.26 +      Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   68.27          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   68.28    in
   68.29      (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
    69.1 --- a/src/Pure/Isar/specification.ML	Thu Jun 09 15:14:21 2011 +0200
    69.2 +++ b/src/Pure/Isar/specification.ML	Thu Jun 09 23:30:18 2011 +0200
    69.3 @@ -93,7 +93,7 @@
    69.4        (case duplicates (op =) commons of [] => ()
    69.5        | dups => error ("Duplicate local variables " ^ commas_quote dups));
    69.6      val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
    69.7 -    val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
    69.8 +    val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
    69.9      val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
   69.10  
   69.11      fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
    70.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Jun 09 15:14:21 2011 +0200
    70.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Jun 09 23:30:18 2011 +0200
    70.3 @@ -29,7 +29,7 @@
    70.4  fun variant a ctxt =
    70.5    let
    70.6      val names = Names.get ctxt;
    70.7 -    val ([b], names') = Name.variants [a] names;
    70.8 +    val (b, names') = Name.variant a names;
    70.9      val ctxt' = Names.put names' ctxt;
   70.10    in (b, ctxt') end;
   70.11  
    71.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jun 09 15:14:21 2011 +0200
    71.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jun 09 23:30:18 2011 +0200
    71.3 @@ -200,7 +200,7 @@
    71.4      fun rew_term Ts t =
    71.5        let
    71.6          val frees =
    71.7 -          map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
    71.8 +          map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
    71.9          val t' = r (subst_bounds (frees, t));
   71.10          fun strip [] t = t
   71.11            | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
    72.1 --- a/src/Pure/Proof/proofchecker.ML	Thu Jun 09 15:14:21 2011 +0200
    72.2 +++ b/src/Pure/Proof/proofchecker.ML	Thu Jun 09 23:30:18 2011 +0200
    72.3 @@ -100,7 +100,7 @@
    72.4  
    72.5        | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
    72.6            let
    72.7 -            val ([x], names') = Name.variants [s] names;
    72.8 +            val (x, names') = Name.variant s names;
    72.9              val thm = thm_of ((x, T) :: vs, names') Hs prf
   72.10            in
   72.11              Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
    73.1 --- a/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:14:21 2011 +0200
    73.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 23:30:18 2011 +0200
    73.3 @@ -241,7 +241,7 @@
    73.4            val rangeT = Term.range_type typ handle Match =>
    73.5              err_in_mfix "Missing structure argument for indexed syntax" mfix;
    73.6  
    73.7 -          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
    73.8 +          val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
    73.9            val (xs1, xs2) = chop (find_index is_index args) xs;
   73.10            val i = Ast.Variable "i";
   73.11            val lhs = Ast.mk_appl (Ast.Constant indexed_const)
    74.1 --- a/src/Pure/Syntax/syntax_trans.ML	Thu Jun 09 15:14:21 2011 +0200
    74.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Thu Jun 09 23:30:18 2011 +0200
    74.3 @@ -439,7 +439,7 @@
    74.4  (* dependent / nondependent quantifiers *)
    74.5  
    74.6  fun var_abs mark (x, T, b) =
    74.7 -  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
    74.8 +  let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
    74.9    in (x', subst_bound (mark (x', T), b)) end;
   74.10  
   74.11  val variant_abs = var_abs Free;
    75.1 --- a/src/Pure/axclass.ML	Thu Jun 09 15:14:21 2011 +0200
    75.2 +++ b/src/Pure/axclass.ML	Thu Jun 09 23:30:18 2011 +0200
    75.3 @@ -265,7 +265,7 @@
    75.4        |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
    75.5              c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
    75.6  
    75.7 -    val names = Name.invents Name.context Name.aT (length Ss);
    75.8 +    val names = Name.invent Name.context Name.aT (length Ss);
    75.9      val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
   75.10  
   75.11      val completions = super_class_completions |> map (fn c1 =>
   75.12 @@ -445,7 +445,7 @@
   75.13      val (th', thy') = Global_Theory.store_thm
   75.14        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
   75.15  
   75.16 -    val args = Name.names Name.context Name.aT Ss;
   75.17 +    val args = Name.invent_names Name.context Name.aT Ss;
   75.18      val T = Type (t, map TFree args);
   75.19      val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
   75.20  
    76.1 --- a/src/Pure/build-jars	Thu Jun 09 15:14:21 2011 +0200
    76.2 +++ b/src/Pure/build-jars	Thu Jun 09 23:30:18 2011 +0200
    76.3 @@ -6,6 +6,53 @@
    76.4  #
    76.5  # Requires proper Isabelle settings environment.
    76.6  
    76.7 +## sources
    76.8 +
    76.9 +declare -a SOURCES=(
   76.10 +  Concurrent/future.scala
   76.11 +  Concurrent/simple_thread.scala
   76.12 +  Concurrent/volatile.scala
   76.13 +  General/exn.scala
   76.14 +  General/timing.scala
   76.15 +  General/linear_set.scala
   76.16 +  General/markup.scala
   76.17 +  General/position.scala
   76.18 +  General/pretty.scala
   76.19 +  General/scan.scala
   76.20 +  General/sha1.scala
   76.21 +  General/symbol.scala
   76.22 +  General/xml.scala
   76.23 +  General/xml_data.scala
   76.24 +  General/yxml.scala
   76.25 +  Isar/keyword.scala
   76.26 +  Isar/outer_syntax.scala
   76.27 +  Isar/parse.scala
   76.28 +  Isar/token.scala
   76.29 +  PIDE/command.scala
   76.30 +  PIDE/document.scala
   76.31 +  PIDE/isar_document.scala
   76.32 +  PIDE/markup_tree.scala
   76.33 +  PIDE/text.scala
   76.34 +  System/cygwin.scala
   76.35 +  System/download.scala
   76.36 +  System/event_bus.scala
   76.37 +  System/gui_setup.scala
   76.38 +  System/isabelle_process.scala
   76.39 +  System/isabelle_syntax.scala
   76.40 +  System/isabelle_system.scala
   76.41 +  System/platform.scala
   76.42 +  System/session.scala
   76.43 +  System/session_manager.scala
   76.44 +  System/standard_system.scala
   76.45 +  System/swing_thread.scala
   76.46 +  Thy/completion.scala
   76.47 +  Thy/html.scala
   76.48 +  Thy/thy_header.scala
   76.49 +  Thy/thy_syntax.scala
   76.50 +  library.scala
   76.51 +  package.scala
   76.52 +)
   76.53 +
   76.54  
   76.55  ## diagnostics
   76.56  
   76.57 @@ -61,51 +108,6 @@
   76.58  
   76.59  ## dependencies
   76.60  
   76.61 -declare -a SOURCES=(
   76.62 -  Concurrent/future.scala
   76.63 -  Concurrent/simple_thread.scala
   76.64 -  Concurrent/volatile.scala
   76.65 -  General/exn.scala
   76.66 -  General/timing.scala
   76.67 -  General/linear_set.scala
   76.68 -  General/markup.scala
   76.69 -  General/position.scala
   76.70 -  General/pretty.scala
   76.71 -  General/scan.scala
   76.72 -  General/sha1.scala
   76.73 -  General/symbol.scala
   76.74 -  General/xml.scala
   76.75 -  General/xml_data.scala
   76.76 -  General/yxml.scala
   76.77 -  Isar/keyword.scala
   76.78 -  Isar/outer_syntax.scala
   76.79 -  Isar/parse.scala
   76.80 -  Isar/token.scala
   76.81 -  PIDE/command.scala
   76.82 -  PIDE/document.scala
   76.83 -  PIDE/isar_document.scala
   76.84 -  PIDE/markup_tree.scala
   76.85 -  PIDE/text.scala
   76.86 -  System/cygwin.scala
   76.87 -  System/download.scala
   76.88 -  System/event_bus.scala
   76.89 -  System/gui_setup.scala
   76.90 -  System/isabelle_process.scala
   76.91 -  System/isabelle_syntax.scala
   76.92 -  System/isabelle_system.scala
   76.93 -  System/platform.scala
   76.94 -  System/session.scala
   76.95 -  System/session_manager.scala
   76.96 -  System/standard_system.scala
   76.97 -  System/swing_thread.scala
   76.98 -  Thy/completion.scala
   76.99 -  Thy/html.scala
  76.100 -  Thy/thy_header.scala
  76.101 -  Thy/thy_syntax.scala
  76.102 -  library.scala
  76.103 -  package.scala
  76.104 -)
  76.105 -
  76.106  TARGET_DIR="$ISABELLE_HOME/lib/classes"
  76.107  PURE_JAR="$TARGET_DIR/Pure.jar"
  76.108  FULL_JAR="$TARGET_DIR/isabelle-scala.jar"
    77.1 --- a/src/Pure/codegen.ML	Thu Jun 09 15:14:21 2011 +0200
    77.2 +++ b/src/Pure/codegen.ML	Thu Jun 09 23:30:18 2011 +0200
    77.3 @@ -273,7 +273,7 @@
    77.4  
    77.5  fun preprocess_term thy t =
    77.6    let
    77.7 -    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
    77.8 +    val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
    77.9      (* fake definition *)
   77.10      val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
   77.11      fun err () = error "preprocess_term: bad preprocessor"
    78.1 --- a/src/Pure/conjunction.ML	Thu Jun 09 15:14:21 2011 +0200
    78.2 +++ b/src/Pure/conjunction.ML	Thu Jun 09 23:30:18 2011 +0200
    78.3 @@ -130,7 +130,7 @@
    78.4  local
    78.5  
    78.6  fun conjs thy n =
    78.7 -  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
    78.8 +  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
    78.9    in (As, mk_conjunction_balanced As) end;
   78.10  
   78.11  val B = read_prop "B";
    79.1 --- a/src/Pure/conv.ML	Thu Jun 09 15:14:21 2011 +0200
    79.2 +++ b/src/Pure/conv.ML	Thu Jun 09 23:30:18 2011 +0200
    79.3 @@ -162,7 +162,7 @@
    79.4      val lhs = Thm.lhs_of rule1;
    79.5      val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    79.6    in
    79.7 -    Drule.instantiate (Thm.match (lhs, ct)) rule2
    79.8 +    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
    79.9        handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   79.10    end;
   79.11  
    80.1 --- a/src/Pure/display.ML	Thu Jun 09 15:14:21 2011 +0200
    80.2 +++ b/src/Pure/display.ML	Thu Jun 09 23:30:18 2011 +0200
    80.3 @@ -156,7 +156,7 @@
    80.4      val tfrees = map (fn v => TFree (v, []));
    80.5      fun pretty_type syn (t, (Type.LogicalType n)) =
    80.6            if syn then NONE
    80.7 -          else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
    80.8 +          else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
    80.9        | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
   80.10            if syn <> syn' then NONE
   80.11            else SOME (Pretty.block
    81.1 --- a/src/Pure/drule.ML	Thu Jun 09 15:14:21 2011 +0200
    81.2 +++ b/src/Pure/drule.ML	Thu Jun 09 23:30:18 2011 +0200
    81.3 @@ -24,7 +24,7 @@
    81.4    val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
    81.5    val implies_elim_list: thm -> thm list -> thm
    81.6    val implies_intr_list: cterm list -> thm -> thm
    81.7 -  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    81.8 +  val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    81.9    val zero_var_indexes_list: thm list -> thm list
   81.10    val zero_var_indexes: thm -> thm
   81.11    val implies_intr_hyps: thm -> thm
   81.12 @@ -110,7 +110,6 @@
   81.13    val comp_no_flatten: thm * int -> int -> thm -> thm
   81.14    val rename_bvars: (string * string) list -> thm -> thm
   81.15    val rename_bvars': string option list -> thm -> thm
   81.16 -  val incr_type_indexes: int -> thm -> thm
   81.17    val incr_indexes: thm -> thm -> thm
   81.18    val incr_indexes2: thm -> thm -> thm -> thm
   81.19    val remdups_rl: thm
   81.20 @@ -337,7 +336,7 @@
   81.21         [] => (fth, fn x => x)
   81.22       | vars =>
   81.23           let fun newName (Var(ix,_), (pairs,used)) =
   81.24 -                   let val v = Name.variant used (string_of_indexname ix)
   81.25 +                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   81.26                     in  ((ix,v)::pairs, v::used)  end;
   81.27               val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
   81.28                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   81.29 @@ -803,13 +802,6 @@
   81.30  
   81.31  (* var indexes *)
   81.32  
   81.33 -(*Increment the indexes of only the type variables*)
   81.34 -fun incr_type_indexes inc th =
   81.35 -  let val tvs = OldTerm.term_tvars (prop_of th)
   81.36 -      and thy = Thm.theory_of_thm th
   81.37 -      fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
   81.38 -  in Thm.instantiate (map inc_tvar tvs, []) th end;
   81.39 -
   81.40  fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
   81.41  
   81.42  fun incr_indexes2 th1 th2 =
   81.43 @@ -829,8 +821,7 @@
   81.44  
   81.45  (*** Instantiate theorem th, reading instantiations in theory thy ****)
   81.46  
   81.47 -(*Version that normalizes the result: Thm.instantiate no longer does that*)
   81.48 -fun instantiate instpair th =
   81.49 +fun instantiate_normalize instpair th =
   81.50    Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
   81.51  
   81.52  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   81.53 @@ -862,7 +853,7 @@
   81.54          let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
   81.55          in (inst ct, inst cu) end
   81.56        fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T))
   81.57 -  in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   81.58 +  in  instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   81.59    handle TERM _ =>
   81.60             raise THM("cterm_instantiate: incompatible theories",0,[th])
   81.61         | TYPE (msg, _, _) => raise THM(msg, 0, [th])
    82.1 --- a/src/Pure/logic.ML	Thu Jun 09 15:14:21 2011 +0200
    82.2 +++ b/src/Pure/logic.ML	Thu Jun 09 23:30:18 2011 +0200
    82.3 @@ -253,7 +253,7 @@
    82.4  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
    82.5  
    82.6  fun mk_arities (t, Ss, S) =
    82.7 -  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
    82.8 +  let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
    82.9    in map (fn c => mk_of_class (T, c)) S end;
   82.10  
   82.11  fun dest_arity tm =
   82.12 @@ -279,7 +279,7 @@
   82.13      val extra = fold (Sorts.remove_sort o #2) present shyps;
   82.14  
   82.15      val n = length present;
   82.16 -    val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
   82.17 +    val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
   82.18  
   82.19      val present_map =
   82.20        map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
    83.1 --- a/src/Pure/more_thm.ML	Thu Jun 09 15:14:21 2011 +0200
    83.2 +++ b/src/Pure/more_thm.ML	Thu Jun 09 23:30:18 2011 +0200
    83.3 @@ -341,7 +341,7 @@
    83.4  fun stripped_sorts thy t =
    83.5    let
    83.6      val tfrees = rev (map TFree (Term.add_tfrees t []));
    83.7 -    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
    83.8 +    val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
    83.9      val strip = tfrees ~~ tfrees';
   83.10      val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
   83.11      val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
    84.1 --- a/src/Pure/name.ML	Thu Jun 09 15:14:21 2011 +0200
    84.2 +++ b/src/Pure/name.ML	Thu Jun 09 23:30:18 2011 +0200
    84.3 @@ -21,12 +21,11 @@
    84.4    val make_context: string list -> context
    84.5    val declare: string -> context -> context
    84.6    val is_declared: context -> string -> bool
    84.7 -  val invents: context -> string -> int -> string list
    84.8 -  val names: context -> string -> 'a list -> (string * 'a) list
    84.9 +  val invent: context -> string -> int -> string list
   84.10 +  val invent_names: context -> string -> 'a list -> (string * 'a) list
   84.11    val invent_list: string list -> string -> int -> string list
   84.12 -  val variants: string list -> context -> string list * context
   84.13 +  val variant: string -> context -> string * context
   84.14    val variant_list: string list -> string list -> string list
   84.15 -  val variant: string list -> string -> string
   84.16    val desymbolize: bool -> string -> string
   84.17  end;
   84.18  
   84.19 @@ -95,28 +94,26 @@
   84.20  fun make_context used = fold declare used context;
   84.21  
   84.22  
   84.23 -(* invents *)
   84.24 +(* invent names *)
   84.25  
   84.26 -fun invents ctxt =
   84.27 +fun invent ctxt =
   84.28    let
   84.29      fun invs _ 0 = []
   84.30        | invs x n =
   84.31 -          let val x' = Symbol.bump_string x in
   84.32 -            if is_declared ctxt x then invs x' n
   84.33 -            else x :: invs x' (n - 1)
   84.34 -          end;
   84.35 +          let val x' = Symbol.bump_string x
   84.36 +          in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
   84.37    in invs o clean end;
   84.38  
   84.39 -fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
   84.40 +fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
   84.41  
   84.42 -val invent_list = invents o make_context;
   84.43 +val invent_list = invent o make_context;
   84.44  
   84.45  
   84.46  (* variants *)
   84.47  
   84.48  (*makes a variant of a name distinct from already used names in a
   84.49    context; preserves a suffix of underscores "_"*)
   84.50 -val variants = fold_map (fn name => fn ctxt =>
   84.51 +fun variant name ctxt =
   84.52    let
   84.53      fun vary x =
   84.54        (case declared ctxt x of
   84.55 @@ -134,10 +131,9 @@
   84.56              |> x0 <> x' ? declare_renaming (x0, x')
   84.57              |> declare x';
   84.58          in (x', ctxt') end;
   84.59 -  in (x' ^ replicate_string n "_", ctxt') end);
   84.60 +  in (x' ^ replicate_string n "_", ctxt') end;
   84.61  
   84.62 -fun variant_list used names = #1 (make_context used |> variants names);
   84.63 -fun variant used = singleton (variant_list used);
   84.64 +fun variant_list used names = #1 (make_context used |> fold_map variant names);
   84.65  
   84.66  
   84.67  (* names conforming to typical requirements of identifiers in the world outside *)
    85.1 --- a/src/Pure/proofterm.ML	Thu Jun 09 15:14:21 2011 +0200
    85.2 +++ b/src/Pure/proofterm.ML	Thu Jun 09 23:30:18 2011 +0200
    85.3 @@ -657,7 +657,7 @@
    85.4        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    85.5      val used = Name.context
    85.6        |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
    85.7 -    val fmap = fs ~~ #1 (Name.variants (map fst fs) used);
    85.8 +    val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
    85.9      fun thaw (f as (a, S)) =
   85.10        (case AList.lookup (op =) fmap f of
   85.11          NONE => TFree f
   85.12 @@ -668,7 +668,7 @@
   85.13  local
   85.14  
   85.15  fun new_name (ix, (pairs,used)) =
   85.16 -  let val v = Name.variant used (string_of_indexname ix)
   85.17 +  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   85.18    in  ((ix, v) :: pairs, v :: used)  end;
   85.19  
   85.20  fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
   85.21 @@ -952,7 +952,7 @@
   85.22  
   85.23  fun canonical_instance typs =
   85.24    let
   85.25 -    val names = Name.invents Name.context Name.aT (length typs);
   85.26 +    val names = Name.invent Name.context Name.aT (length typs);
   85.27      val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
   85.28    in instantiate (instT, []) end;
   85.29  
    86.1 --- a/src/Pure/raw_simplifier.ML	Thu Jun 09 15:14:21 2011 +0200
    86.2 +++ b/src/Pure/raw_simplifier.ML	Thu Jun 09 23:30:18 2011 +0200
    86.3 @@ -305,7 +305,7 @@
    86.4  fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
    86.5    let
    86.6      val names = Term.declare_term_names t Name.context;
    86.7 -    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
    86.8 +    val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
    86.9      fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
   86.10    in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
   86.11  
    87.1 --- a/src/Pure/term.ML	Thu Jun 09 15:14:21 2011 +0200
    87.2 +++ b/src/Pure/term.ML	Thu Jun 09 23:30:18 2011 +0200
    87.3 @@ -514,7 +514,8 @@
    87.4  val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
    87.5  
    87.6  fun variant_frees t frees =
    87.7 -  fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
    87.8 +  fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
    87.9 +    map snd frees;
   87.10  
   87.11  fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   87.12  
   87.13 @@ -705,7 +706,7 @@
   87.14      fun strip_abs t (0, used) = (([], t), (0, used))
   87.15        | strip_abs (Abs (v, T, t)) (k, used) =
   87.16            let
   87.17 -            val ([v'], used') = Name.variants [v] used;
   87.18 +            val (v', used') = Name.variant v used;
   87.19              val t' = subst_bound (Free (v', T), t);
   87.20              val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   87.21            in (((v', T) :: vs, t''), (k', used'')) end
   87.22 @@ -713,7 +714,7 @@
   87.23      fun expand_eta [] t _ = ([], t)
   87.24        | expand_eta (T::Ts) t used =
   87.25            let
   87.26 -            val ([v], used') = Name.variants [""] used;
   87.27 +            val (v, used') = Name.variant "" used;
   87.28              val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   87.29            in ((v, T) :: vs, t') end;
   87.30      val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   87.31 @@ -936,7 +937,8 @@
   87.32        | name_clash (Abs (_, _, t)) = name_clash t
   87.33        | name_clash _ = false;
   87.34    in
   87.35 -    if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
   87.36 +    if name_clash body then
   87.37 +      dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
   87.38      else (x, subst_bound (Free (x, T), body))
   87.39    end;
   87.40  
   87.41 @@ -955,7 +957,7 @@
   87.42    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
   87.43  
   87.44  fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
   87.45 -      let val [x] = Name.invents used Name.uu 1
   87.46 +      let val [x] = Name.invent used Name.uu 1
   87.47        in (Free (Name.internal x, T), Name.declare x used) end
   87.48    | free_dummy_patterns (Abs (x, T, b)) used =
   87.49        let val (b', used') = free_dummy_patterns b used
    88.1 --- a/src/Pure/term_subst.ML	Thu Jun 09 15:14:21 2011 +0200
    88.2 +++ b/src/Pure/term_subst.ML	Thu Jun 09 23:30:18 2011 +0200
    88.3 @@ -163,7 +163,7 @@
    88.4  fun zero_var_inst vars =
    88.5    fold (fn v as ((x, i), X) => fn (inst, used) =>
    88.6      let
    88.7 -      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
    88.8 +      val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
    88.9      in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
   88.10    vars ([], Name.context) |> #1;
   88.11  
    89.1 --- a/src/Pure/type.ML	Thu Jun 09 15:14:21 2011 +0200
    89.2 +++ b/src/Pure/type.ML	Thu Jun 09 23:30:18 2011 +0200
    89.3 @@ -345,7 +345,7 @@
    89.4        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    89.5      val used = Name.context
    89.6        |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
    89.7 -    val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
    89.8 +    val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
    89.9      fun thaw (f as (_, S)) =
   89.10        (case AList.lookup (op =) fmap f of
   89.11          NONE => TFree f
   89.12 @@ -358,7 +358,7 @@
   89.13  local
   89.14  
   89.15  fun new_name (ix, (pairs, used)) =
   89.16 -  let val v = Name.variant used (string_of_indexname ix)
   89.17 +  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   89.18    in ((ix, v) :: pairs, v :: used) end;
   89.19  
   89.20  fun freeze_one alist (ix, sort) =
    90.1 --- a/src/Pure/type_infer.ML	Thu Jun 09 15:14:21 2011 +0200
    90.2 +++ b/src/Pure/type_infer.ML	Thu Jun 09 23:30:18 2011 +0200
    90.3 @@ -96,7 +96,7 @@
    90.4      val used =
    90.5        (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
    90.6      val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
    90.7 -    val names = Name.invents used ("?" ^ Name.aT) (length parms);
    90.8 +    val names = Name.invent used ("?" ^ Name.aT) (length parms);
    90.9      val tab = Vartab.make (parms ~~ names);
   90.10  
   90.11      fun finish_typ T =
   90.12 @@ -117,7 +117,7 @@
   90.13      fun subst_param (xi, S) (inst, used) =
   90.14        if is_param xi then
   90.15          let
   90.16 -          val [a] = Name.invents used Name.aT 1;
   90.17 +          val [a] = Name.invent used Name.aT 1;
   90.18            val used' = Name.declare a used;
   90.19          in (((xi, S), TFree (a, S)) :: inst, used') end
   90.20        else (inst, used);
    91.1 --- a/src/Pure/variable.ML	Thu Jun 09 15:14:21 2011 +0200
    91.2 +++ b/src/Pure/variable.ML	Thu Jun 09 23:30:18 2011 +0200
    91.3 @@ -255,7 +255,7 @@
    91.4  fun variant_frees ctxt ts frees =
    91.5    let
    91.6      val names = names_of (fold declare_names ts ctxt);
    91.7 -    val xs = fst (Name.variants (map #1 frees) names);
    91.8 +    val xs = fst (fold_map Name.variant (map #1 frees) names);
    91.9    in xs ~~ map snd frees end;
   91.10  
   91.11  
   91.12 @@ -365,7 +365,7 @@
   91.13      val xs = map check_name bs;
   91.14      val names = names_of ctxt;
   91.15      val (xs', names') =
   91.16 -      if is_body ctxt then Name.variants xs names |>> map Name.skolem
   91.17 +      if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
   91.18        else (xs, fold Name.declare xs names);
   91.19    in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
   91.20  
   91.21 @@ -373,7 +373,7 @@
   91.22    let
   91.23      val names = names_of ctxt;
   91.24      val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
   91.25 -    val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
   91.26 +    val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
   91.27    in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
   91.28  
   91.29  end;
   91.30 @@ -391,7 +391,7 @@
   91.31  
   91.32  fun invent_types Ss ctxt =
   91.33    let
   91.34 -    val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
   91.35 +    val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
   91.36      val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   91.37    in (tfrees, ctxt') end;
   91.38  
    92.1 --- a/src/Tools/Code/code_haskell.ML	Thu Jun 09 15:14:21 2011 +0200
    92.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jun 09 23:30:18 2011 +0200
    92.3 @@ -264,13 +264,12 @@
    92.4    let
    92.5      fun namify_fun upper base (nsp_fun, nsp_typ) =
    92.6        let
    92.7 -        val (base', nsp_fun') = yield_singleton Name.variants
    92.8 -          (if upper then first_upper base else base) nsp_fun;
    92.9 +        val (base', nsp_fun') =
   92.10 +          Name.variant (if upper then first_upper base else base) nsp_fun;
   92.11        in (base', (nsp_fun', nsp_typ)) end;
   92.12      fun namify_typ base (nsp_fun, nsp_typ) =
   92.13        let
   92.14 -        val (base', nsp_typ') = yield_singleton Name.variants
   92.15 -          (first_upper base) nsp_typ
   92.16 +        val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
   92.17        in (base', (nsp_fun, nsp_typ')) end;
   92.18      fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
   92.19        | namify_stmt (Code_Thingol.Fun _) = namify_fun false
    93.1 --- a/src/Tools/Code/code_ml.ML	Thu Jun 09 15:14:21 2011 +0200
    93.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jun 09 23:30:18 2011 +0200
    93.3 @@ -716,12 +716,12 @@
    93.4    let
    93.5      fun namify_const upper base (nsp_const, nsp_type) =
    93.6        let
    93.7 -        val (base', nsp_const') = yield_singleton Name.variants
    93.8 -          (if upper then first_upper base else base) nsp_const
    93.9 +        val (base', nsp_const') =
   93.10 +          Name.variant (if upper then first_upper base else base) nsp_const
   93.11        in (base', (nsp_const', nsp_type)) end;
   93.12      fun namify_type base (nsp_const, nsp_type) =
   93.13        let
   93.14 -        val (base', nsp_type') = yield_singleton Name.variants base nsp_type
   93.15 +        val (base', nsp_type') = Name.variant base nsp_type
   93.16        in (base', (nsp_const, nsp_type')) end;
   93.17      fun namify_stmt (Code_Thingol.Fun _) = namify_const false
   93.18        | namify_stmt (Code_Thingol.Datatype _) = namify_type
    94.1 --- a/src/Tools/Code/code_namespace.ML	Thu Jun 09 15:14:21 2011 +0200
    94.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Jun 09 23:30:18 2011 +0200
    94.3 @@ -46,8 +46,7 @@
    94.4    let
    94.5      fun alias_fragments name = case module_alias name
    94.6       of SOME name' => Long_Name.explode name'
    94.7 -      | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    94.8 -          (Long_Name.explode name);
    94.9 +      | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
   94.10      val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
   94.11    in
   94.12      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
    95.1 --- a/src/Tools/Code/code_printer.ML	Thu Jun 09 15:14:21 2011 +0200
    95.2 +++ b/src/Tools/Code/code_printer.ML	Thu Jun 09 23:30:18 2011 +0200
    95.3 @@ -165,7 +165,7 @@
    95.4  
    95.5  fun intro_vars names (namemap, namectxt) =
    95.6    let
    95.7 -    val (names', namectxt') = Name.variants names namectxt;
    95.8 +    val (names', namectxt') = fold_map Name.variant names namectxt;
    95.9      val namemap' = fold2 (curry Symtab.update) names names' namemap;
   95.10    in (namemap', namectxt') end;
   95.11  
   95.12 @@ -184,9 +184,9 @@
   95.13      fun fillup_param _ (_, SOME v) = v
   95.14        | fillup_param x (i, NONE) = x ^ string_of_int i;
   95.15      val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
   95.16 -    val x = Name.variant (map_filter I fished1) "x";
   95.17 +    val x = singleton (Name.variant_list (map_filter I fished1)) "x";
   95.18      val fished2 = map_index (fillup_param x) fished1;
   95.19 -    val (fished3, _) = Name.variants fished2 Name.context;
   95.20 +    val (fished3, _) = fold_map Name.variant fished2 Name.context;
   95.21      val vars' = intro_vars fished3 vars;
   95.22    in map (lookup_var vars') fished3 end;
   95.23  
    96.1 --- a/src/Tools/Code/code_scala.ML	Thu Jun 09 15:14:21 2011 +0200
    96.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jun 09 23:30:18 2011 +0200
    96.3 @@ -149,7 +149,7 @@
    96.4      fun print_def name (vs, ty) [] =
    96.5            let
    96.6              val (tys, ty') = Code_Thingol.unfold_fun ty;
    96.7 -            val params = Name.invents (snd reserved) "a" (length tys);
    96.8 +            val params = Name.invent (snd reserved) "a" (length tys);
    96.9              val tyvars = intro_tyvars vs reserved;
   96.10              val vars = intro_vars params reserved;
   96.11            in
   96.12 @@ -214,7 +214,7 @@
   96.13                      (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
   96.14                      (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
   96.15                        ["final", "case", "class", deresolve co]) vs_args)
   96.16 -                    (Name.names (snd reserved) "a" tys),
   96.17 +                    (Name.invent_names (snd reserved) "a" tys),
   96.18                      str "extends",
   96.19                      applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
   96.20                        ((str o deresolve) name) vs
   96.21 @@ -238,9 +238,9 @@
   96.22              fun print_classparam_def (classparam, ty) =
   96.23                let
   96.24                  val (tys, ty) = Code_Thingol.unfold_fun ty;
   96.25 -                val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
   96.26 +                val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1;
   96.27                  val proto_vars = intro_vars [implicit_name] reserved;
   96.28 -                val auxs = Name.invents (snd proto_vars) "a" (length tys);
   96.29 +                val auxs = Name.invent (snd proto_vars) "a" (length tys);
   96.30                  val vars = intro_vars auxs proto_vars;
   96.31                in
   96.32                  concat [str "def", constraint (Pretty.block [applify "(" ")"
   96.33 @@ -267,7 +267,7 @@
   96.34              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   96.35              fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   96.36                let
   96.37 -                val aux_tys = Name.names (snd reserved) "a" tys;
   96.38 +                val aux_tys = Name.invent_names (snd reserved) "a" tys;
   96.39                  val auxs = map fst aux_tys;
   96.40                  val vars = intro_vars auxs reserved;
   96.41                  val aux_abstr = if null auxs then [] else [enum "," "(" ")"
   96.42 @@ -294,16 +294,16 @@
   96.43        in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
   96.44      fun namify_class base ((nsp_class, nsp_object), nsp_common) =
   96.45        let
   96.46 -        val (base', nsp_class') = yield_singleton Name.variants base nsp_class
   96.47 +        val (base', nsp_class') = Name.variant base nsp_class
   96.48        in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   96.49      fun namify_object base ((nsp_class, nsp_object), nsp_common) =
   96.50        let
   96.51 -        val (base', nsp_object') = yield_singleton Name.variants base nsp_object
   96.52 +        val (base', nsp_object') = Name.variant base nsp_object
   96.53        in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   96.54      fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
   96.55        let
   96.56          val (base', nsp_common') =
   96.57 -          yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
   96.58 +          Name.variant (if upper then first_upper base else base) nsp_common
   96.59        in
   96.60          (base',
   96.61            ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
    97.1 --- a/src/Tools/Code/code_target.ML	Thu Jun 09 15:14:21 2011 +0200
    97.2 +++ b/src/Tools/Code/code_target.ML	Thu Jun 09 23:30:18 2011 +0200
    97.3 @@ -416,7 +416,7 @@
    97.4    let
    97.5      val _ = if Code_Thingol.contains_dict_var t then
    97.6        error "Term to be evaluated contains free dictionaries" else ();
    97.7 -    val v' = Name.variant (map fst vs) "a";
    97.8 +    val v' = singleton (Name.variant_list (map fst vs)) "a";
    97.9      val vs' = (v', []) :: vs;
   97.10      val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
   97.11      val value_name = "Value.value.value"
    98.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 09 15:14:21 2011 +0200
    98.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 09 23:30:18 2011 +0200
    98.3 @@ -237,7 +237,7 @@
    98.4    | unfold_abs_eta tys t =
    98.5        let
    98.6          val ctxt = fold_varnames Name.declare t Name.context;
    98.7 -        val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
    98.8 +        val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
    98.9        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
   98.10  
   98.11  fun eta_expand k (c as (name, (_, tys)), ts) =
   98.12 @@ -248,7 +248,7 @@
   98.13        then error ("Impossible eta-expansion for constant " ^ quote name) else ();
   98.14      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
   98.15      val vs_tys = (map o apfst) SOME
   98.16 -      (Name.names ctxt "a" ((take l o drop j) tys));
   98.17 +      (Name.invent_names ctxt "a" ((take l o drop j) tys));
   98.18    in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
   98.19  
   98.20  fun contains_dict_var t =
   98.21 @@ -354,7 +354,7 @@
   98.22  
   98.23  fun add_variant update (thing, name) (tab, used) =
   98.24    let
   98.25 -    val (name', used') = yield_singleton Name.variants name used;
   98.26 +    val (name', used') = Name.variant name used;
   98.27      val tab' = update (thing, name') tab;
   98.28    in (tab', used') end;
   98.29  
   98.30 @@ -671,7 +671,7 @@
   98.31      val classparams = these_classparams class;
   98.32      val further_classparams = maps these_classparams
   98.33        ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
   98.34 -    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   98.35 +    val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   98.36      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   98.37      val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
   98.38        Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   98.39 @@ -820,7 +820,7 @@
   98.40        val k = length ts;
   98.41        val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
   98.42        val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
   98.43 -      val vs = Name.names ctxt "a" tys;
   98.44 +      val vs = Name.invent_names ctxt "a" tys;
   98.45      in
   98.46        fold_map (translate_typ thy algbr eqngr permissive) tys
   98.47        ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
    99.1 --- a/src/Tools/Code/lib/Tools/codegen	Thu Jun 09 15:14:21 2011 +0200
    99.2 +++ b/src/Tools/Code/lib/Tools/codegen	Thu Jun 09 23:30:18 2011 +0200
    99.3 @@ -51,7 +51,7 @@
    99.4  ## invoke code generation
    99.5  
    99.6  FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
    99.7 -  (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
    99.8 +  (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
    99.9    handle _ => OS.Process.exit OS.Process.failure;"
   99.10  
   99.11  ACTUAL_CMD="val thyname = \"$THYNAME\"; \
   100.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 15:14:21 2011 +0200
   100.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 23:30:18 2011 +0200
   100.3 @@ -190,7 +190,7 @@
   100.4        val tvars = List.foldr OldTerm.add_term_tvars [] ts;
   100.5        val (names',renamings) = 
   100.6            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   100.7 -                         let val n2 = Name.variant Ns n in 
   100.8 +                         let val n2 = singleton (Name.variant_list Ns) n in 
   100.9                             (n2::Ns, (tv, (n2,s))::Rs)
  100.10                           end) (tfree_names @ names,[]) tvars;
  100.11      in renamings end;
  100.12 @@ -223,7 +223,7 @@
  100.13        val Ns = List.foldr OldTerm.add_term_names names ts;
  100.14        val (_,renamings) = 
  100.15            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
  100.16 -                    let val n2 = Name.variant Ns n in
  100.17 +                    let val n2 = singleton (Name.variant_list Ns) n in
  100.18                        (n2 :: Ns, (v, (n2,ty)) :: Rs)
  100.19                      end) ((Ns,[]), vars);
  100.20      in renamings end;
   101.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 15:14:21 2011 +0200
   101.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 23:30:18 2011 +0200
   101.3 @@ -101,7 +101,7 @@
   101.4        val names = usednames_of_thm rule;
   101.5        val (fromnames,tonames,names2,Ts') = 
   101.6            Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
   101.7 -                    let val n2 = Name.variant names n in
   101.8 +                    let val n2 = singleton (Name.variant_list names) n in
   101.9                        (ctermify (Free(faken,ty)) :: rnf,
  101.10                         ctermify (Free(n2,ty)) :: rnt, 
  101.11                         n2 :: names,
  101.12 @@ -146,7 +146,7 @@
  101.13        val vars_to_fix = union (op =) termvars cond_vs;
  101.14        val (renamings, names2) = 
  101.15            List.foldr (fn (((n,i),ty), (vs, names')) => 
  101.16 -                    let val n' = Name.variant names' n in
  101.17 +                    let val n' = singleton (Name.variant_list names') n in
  101.18                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
  101.19                      end)
  101.20                  ([], names) vars_to_fix;
  101.21 @@ -154,7 +154,7 @@
  101.22  
  101.23  (* make a new fresh typefree instantiation for the given tvar *)
  101.24  fun new_tfree (tv as (ix,sort), (pairs,used)) =
  101.25 -      let val v = Name.variant used (string_of_indexname ix)
  101.26 +      let val v = singleton (Name.variant_list used) (string_of_indexname ix)
  101.27        in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
  101.28  
  101.29  
   102.1 --- a/src/Tools/eqsubst.ML	Thu Jun 09 15:14:21 2011 +0200
   102.2 +++ b/src/Tools/eqsubst.ML	Thu Jun 09 23:30:18 2011 +0200
   102.3 @@ -179,7 +179,7 @@
   102.4  fun fakefree_badbounds Ts t = 
   102.5      let val (FakeTs,Ts,newnames) = 
   102.6              List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   102.7 -                           let val newname = Name.variant usednames n
   102.8 +                           let val newname = singleton (Name.variant_list usednames) n
   102.9                             in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
  102.10                                 (newname,ty)::Ts, 
  102.11                                 newname::usednames) end)
   103.1 --- a/src/Tools/induct.ML	Thu Jun 09 15:14:21 2011 +0200
   103.2 +++ b/src/Tools/induct.ML	Thu Jun 09 23:30:18 2011 +0200
   103.3 @@ -588,9 +588,10 @@
   103.4          val concl = Logic.strip_assums_concl goal;
   103.5        in
   103.6          Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
   103.7 -        |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
   103.8 +        |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
   103.9        end
  103.10 -  end handle General.Subscript => Seq.empty;
  103.11 +  end
  103.12 +  handle General.Subscript => Seq.empty;
  103.13  
  103.14  end;
  103.15  
  103.16 @@ -692,7 +693,7 @@
  103.17        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
  103.18        | add (SOME (NONE, (t, _))) ctxt =
  103.19            let
  103.20 -            val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
  103.21 +            val (s, _) = Name.variant "x" (Variable.names_of ctxt);
  103.22              val ([(lhs, (_, th))], ctxt') =
  103.23                Local_Defs.add_defs [((Binding.name s, NoSyn),
  103.24                  (Thm.empty_binding, t))] ctxt
   104.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 09 15:14:21 2011 +0200
   104.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 09 23:30:18 2011 +0200
   104.3 @@ -7,7 +7,7 @@
   104.4  
   104.5  ## sources
   104.6  
   104.7 -declare -a SOURCE_FILES=(
   104.8 +declare -a SOURCES=(
   104.9    "src/dockable.scala"
  104.10    "src/document_model.scala"
  104.11    "src/document_view.scala"
  104.12 @@ -25,7 +25,7 @@
  104.13    "src/session_dockable.scala"
  104.14  )
  104.15  
  104.16 -declare -a MORE_FILES=(
  104.17 +declare -a RESOURCES=(
  104.18    "src/actions.xml"
  104.19    "src/dockables.xml"
  104.20    "src/Isabelle.props"
  104.21 @@ -169,7 +169,7 @@
  104.22    OUTDATED=true
  104.23  else
  104.24    OUTDATED=false
  104.25 -  for SOURCE in "${SOURCE_FILES[@]}" "${MORE_FILES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
  104.26 +  for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
  104.27    do
  104.28      [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
  104.29      [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
  104.30 @@ -198,7 +198,7 @@
  104.31    mkdir -p dist dist/classes || failed
  104.32  
  104.33    cp -a "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
  104.34 -  cp -a "${MORE_FILES[@]}" dist/classes/.
  104.35 +  cp -a "${RESOURCES[@]}" dist/classes/.
  104.36    cp src/jEdit.props dist/properties/.
  104.37    cp -a src/modes/. dist/modes/.
  104.38  
  104.39 @@ -218,7 +218,7 @@
  104.40      CLASSPATH="$(jvmpath "$CLASSPATH")"
  104.41  
  104.42      exec "$SCALA_HOME/bin/scalac" -unchecked -deprecation \
  104.43 -      -d dist/classes -target:jvm-1.5 "${SOURCE_FILES[@]}"
  104.44 +      -d dist/classes -target:jvm-1.5 "${SOURCES[@]}"
  104.45    ) || fail "Failed to compile sources"
  104.46  
  104.47    cd dist/classes
   105.1 --- a/src/Tools/nbe.ML	Thu Jun 09 15:14:21 2011 +0200
   105.2 +++ b/src/Tools/nbe.ML	Thu Jun 09 23:30:18 2011 +0200
   105.3 @@ -330,7 +330,8 @@
   105.4          val vs = (fold o Code_Thingol.fold_varnames)
   105.5            (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
   105.6          val names = Name.make_context (map fst vs);
   105.7 -        fun declare v k ctxt = let val vs = Name.invents ctxt v k
   105.8 +        fun declare v k ctxt =
   105.9 +          let val vs = Name.invent ctxt v k
  105.10            in (vs, fold Name.declare vs ctxt) end;
  105.11          val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
  105.12            then declare v (k - 1) #>> (fn vs => (v, vs))
  105.13 @@ -372,7 +373,7 @@
  105.14      fun assemble_eqns (c, (num_args, (dicts, eqns))) =
  105.15        let
  105.16          val default_args = map nbe_default
  105.17 -          (Name.invent_list [] "a" (num_args - length dicts));
  105.18 +          (Name.invent Name.context "a" (num_args - length dicts));
  105.19          val eqns' = map_index (assemble_eqn c dicts default_args) eqns
  105.20            @ (if c = "" then [] else [(nbe_fun (length eqns) c,
  105.21              [([ml_list (rev (dicts @ default_args))],
  105.22 @@ -421,7 +422,7 @@
  105.23    | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
  105.24        let
  105.25          val names = map snd super_classes @ map fst classparams;
  105.26 -        val params = Name.invent_list [] "d" (length names);
  105.27 +        val params = Name.invent Name.context "d" (length names);
  105.28          fun mk (k, name) =
  105.29            (name, ([(v, [])],
  105.30              [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
   106.1 --- a/src/ZF/Tools/cartprod.ML	Thu Jun 09 15:14:21 2011 +0200
   106.2 +++ b/src/ZF/Tools/cartprod.ML	Thu Jun 09 23:30:18 2011 +0200
   106.3 @@ -108,7 +108,7 @@
   106.4            val newt = ap_split T1 T2 (Var(v,T'))
   106.5            val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
   106.6        in
   106.7 -          remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
   106.8 +          remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
   106.9                                             cterm newt)]) rl)
  106.10        end
  106.11    | split_rule_var (t,T,rl) = rl;
   107.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Jun 09 15:14:21 2011 +0200
   107.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 09 23:30:18 2011 +0200
   107.3 @@ -96,7 +96,7 @@
   107.4                 Syntax.string_of_term ctxt t);
   107.5  
   107.6    (*** Construct the fixedpoint definition ***)
   107.7 -  val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
   107.8 +  val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
   107.9  
  107.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
  107.11  
  107.12 @@ -493,7 +493,7 @@
  107.13         The name "x.1" comes from the "RS spec" !*)
  107.14       val inst =
  107.15           case elem_frees of [_] => I
  107.16 -            | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
  107.17 +            | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
  107.18                                        cterm_of thy1 elem_tuple)]);
  107.19  
  107.20       (*strip quantifier and the implication*)
   108.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Jun 09 15:14:21 2011 +0200
   108.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Jun 09 23:30:18 2011 +0200
   108.3 @@ -139,8 +139,9 @@
   108.4      (** make definition **)
   108.5  
   108.6      (*the recursive argument*)
   108.7 -    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
   108.8 -                        Ind_Syntax.iT)
   108.9 +    val rec_arg =
  108.10 +      Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
  108.11 +        Ind_Syntax.iT)
  108.12  
  108.13      val def_tm = Logic.mk_equals
  108.14                      (subst_bound (rec_arg, fabs),