*** empty log message ***
authorwenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13 ago)
changeset 15703727ef1b8b3ee
parent 15702 2677db44c795
child 15704 93163972dbdc
*** empty log message ***
NEWS
etc/isar-keywords.el
etc/settings
lib/Tools/display
lib/Tools/doc
lib/Tools/mkdir
src/HOL/Import/import_package.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/Provers/classical.ML
src/Provers/induct_method.ML
src/Pure/Isar/ROOT.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/axclass.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/NEWS	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/NEWS	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -6,13 +6,13 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* The type Library.option is no more, along with the exception
     1.8 +* ML: The type Library.option is no more, along with the exception
     1.9    Library.OPTION: Isabelle now uses the standard option type.  The
    1.10    functions the, is_some, is_none, etc. are still in Library, but
    1.11    the constructors are now SOME and NONE instead of Some and None.
    1.12 -  They throw the exception Option.
    1.13 -
    1.14 -* The exception LIST is no more, the standard exceptions Empty and
    1.15 +  They raise the exception Option.
    1.16 +
    1.17 +* ML: The exception LIST is no more, the standard exceptions Empty and
    1.18    Subscript, as well as Library.UnequalLengths are used instead.  This
    1.19    means that function like Library.hd and Library.tl are gone, as the
    1.20    standard hd and tl functions suffice.
    1.21 @@ -42,12 +42,6 @@
    1.22    A simple solution to broken code is to include "open Library" at the
    1.23    beginning of a structure.  Everything after that will be as before.
    1.24  
    1.25 -* Document preparation: new antiquotations @{lhs thm} and @{rhs thm}
    1.26 -  printing the lhs/rhs of definitions, equations, inequations etc. 
    1.27 -
    1.28 -* isatool usedir: new option -f that allows specification of the ML
    1.29 -  file to be used by Isabelle; default is ROOT.ML.
    1.30 -
    1.31  * Theory headers: the new header syntax for Isar theories is
    1.32  
    1.33    theory <name>
    1.34 @@ -145,76 +139,11 @@
    1.35    internally, to allow for use in a context of fixed variables.
    1.36  
    1.37  * Pure/Simplifier: Command "find_rewrites" takes a string and lists all
    1.38 -  equality theorems (not just those with attribute simp!) whose left-hand
    1.39 +  equality theorems (not just those declared as simp!) whose left-hand
    1.40    side matches the term given via the string. In PG the command can be
    1.41    activated via Isabelle -> Show me -> matching rewrites.
    1.42  
    1.43 -* Provers: Simplifier and Classical Reasoner now support proof context
    1.44 -  dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
    1.45 -  components are stored in the theory and patched into the
    1.46 -  simpset/claset when used in an Isar proof context.  Context
    1.47 -  dependent components are maintained by the following theory
    1.48 -  operations:
    1.49 -
    1.50 -    Simplifier.add_context_simprocs
    1.51 -    Simplifier.del_context_simprocs
    1.52 -    Simplifier.set_context_subgoaler
    1.53 -    Simplifier.reset_context_subgoaler
    1.54 -    Simplifier.add_context_looper
    1.55 -    Simplifier.del_context_looper
    1.56 -    Simplifier.add_context_unsafe_solver
    1.57 -    Simplifier.add_context_safe_solver
    1.58 -
    1.59 -    Classical.add_context_safe_wrapper
    1.60 -    Classical.del_context_safe_wrapper
    1.61 -    Classical.add_context_unsafe_wrapper
    1.62 -    Classical.del_context_unsafe_wrapper
    1.63 -
    1.64 -  IMPORTANT NOTE: proof tools (methods etc.) need to use
    1.65 -  local_simpset_of and local_claset_of to instead of the primitive
    1.66 -  Simplifier.get_local_simpset and Classical.get_local_claset,
    1.67 -  respectively, in order to see the context dependent fields!
    1.68 -
    1.69 -* Document preparation: antiquotations now provide the option
    1.70 -  'locale=NAME' to specify an alternative context used for evaluating
    1.71 -  and printing the subsequent argument, as in @{thm [locale=LC]
    1.72 -  fold_commute}, for example.
    1.73 -
    1.74 -* Document preparation: commands 'display_drafts' and 'print_drafts'
    1.75 -  perform simple output of raw sources.  Only those symbols that do
    1.76 -  not require additional LaTeX packages (depending on comments in
    1.77 -  isabellesym.sty) are displayed properly, everything else is left
    1.78 -  verbatim.  We use isatool display and isatool print as front ends;
    1.79 -  these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
    1.80 -  respectively.
    1.81 -
    1.82 -* Document preparation: Proof scripts as well as some other commands
    1.83 -  such as ML or parse/print_translation can now be hidden in the document.
    1.84 -  Hiding is enabled by default, and can be disabled either via the option
    1.85 -  '-H false' of isatool usedir or by resetting the reference variable
    1.86 -  IsarOutput.hide_commands. Additional commands to be hidden may be
    1.87 -  declared using IsarOutput.add_hidden_commands.
    1.88 -
    1.89 -* ML: output via the Isabelle channels of writeln/warning/error
    1.90 -  etc. is now passed through Output.output, with a hook for arbitrary
    1.91 -  transformations depending on the print_mode (cf. Output.add_mode --
    1.92 -  the first active mode that provides a output function wins).
    1.93 -  Already formatted output may be embedded into further text via
    1.94 -  Output.raw; the result of Pretty.string_of/str_of and derived
    1.95 -  functions (string_of_term/cterm/thm etc.) is already marked raw to
    1.96 -  accommodate easy composition of diagnostic messages etc.
    1.97 -  Programmers rarely need to care about Output.output or Output.raw at
    1.98 -  all, with some notable exceptions: Output.output is required when
    1.99 -  bypassing the standard channels (writeln etc.), or in token
   1.100 -  translations to produce properly formatted results; Output.raw is
   1.101 -  required when capturing already output material that will eventually
   1.102 -  be presented to the user a second time.  For the default print mode,
   1.103 -  both Output.output and Output.raw have no effect.
   1.104 -
   1.105 -
   1.106 -*** Isar ***
   1.107 -
   1.108 -* Debugging: new reference Toplevel.debug; default false.
   1.109 +* Isar debugging: new reference Toplevel.debug; default false.
   1.110    Set to make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
   1.111    
   1.112  * Locales:
   1.113 @@ -232,12 +161,33 @@
   1.114    in duplicate.
   1.115    Use print_interps to inspect active interpretations of a particular locale.
   1.116  
   1.117 -* New syntax
   1.118 -
   1.119 -    <theorem_name> (<index>, ..., <index>-<index>, ...)
   1.120 -
   1.121 -  for referring to specific theorems in a named list of theorems via
   1.122 -  indices.
   1.123 +* Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
   1.124 +  selections of theorems in named facts via indices.
   1.125 +
   1.126 +
   1.127 +*** Document preparation ***
   1.128 +
   1.129 +* New antiquotations @{lhs thm} and @{rhs thm} printing the lhs/rhs of
   1.130 +  definitions, equations, inequations etc.
   1.131 +
   1.132 +* Antiquotations now provide the option 'locale=NAME' to specify an
   1.133 +  alternative context used for evaluating and printing the subsequent
   1.134 +  argument, as in @{thm [locale=LC] fold_commute}, for example.
   1.135 +
   1.136 +* Commands 'display_drafts' and 'print_drafts' perform simple output
   1.137 +  of raw sources.  Only those symbols that do not require additional
   1.138 +  LaTeX packages (depending on comments in isabellesym.sty) are
   1.139 +  displayed properly, everything else is left verbatim.  We use
   1.140 +  isatool display and isatool print as front ends; these are subject
   1.141 +  to the DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively.
   1.142 +
   1.143 +* Proof scripts as well as some other commands such as ML or
   1.144 +  parse/print_translation can now be hidden in the document.  Hiding
   1.145 +  is enabled by default, and can be disabled either via the option '-H
   1.146 +  false' of isatool usedir or by resetting the reference variable
   1.147 +  IsarOutput.hide_commands. Additional commands to be hidden may be
   1.148 +  declared using IsarOutput.add_hidden_commands.
   1.149 +
   1.150  
   1.151  *** HOL ***
   1.152  
   1.153 @@ -337,9 +287,6 @@
   1.154    enabled/disabled by the reference use_let_simproc. Potential
   1.155    INCOMPATIBILITY since simplification is more powerful by default.
   1.156   
   1.157 -* HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
   1.158 -  (containing Boolean satisfiability problems) into Isabelle/HOL theories.
   1.159 -
   1.160  
   1.161  *** HOLCF ***
   1.162  
   1.163 @@ -359,6 +306,64 @@
   1.164    the old version is still required for ML proof scripts.
   1.165  
   1.166  
   1.167 +*** System ***
   1.168 +
   1.169 +* HOL: isatool dimacs2hol converts files in DIMACS CNF format
   1.170 +  (containing Boolean satisfiability problems) into Isabelle/HOL
   1.171 +  theories.
   1.172 +
   1.173 +* isatool usedir: option -f allows specification of the ML file to be
   1.174 +  used by Isabelle; default is ROOT.ML.
   1.175 +
   1.176 +* ISABELLE_DOC_FORMAT setting specifies preferred document format (for
   1.177 +  isatool doc, isatool mkdir, display_drafts etc.).
   1.178 +
   1.179 +
   1.180 +*** ML ***
   1.181 +
   1.182 +* Pure: output via the Isabelle channels of writeln/warning/error
   1.183 +  etc. is now passed through Output.output, with a hook for arbitrary
   1.184 +  transformations depending on the print_mode (cf. Output.add_mode --
   1.185 +  the first active mode that provides a output function wins).
   1.186 +  Already formatted output may be embedded into further text via
   1.187 +  Output.raw; the result of Pretty.string_of/str_of and derived
   1.188 +  functions (string_of_term/cterm/thm etc.) is already marked raw to
   1.189 +  accommodate easy composition of diagnostic messages etc.
   1.190 +  Programmers rarely need to care about Output.output or Output.raw at
   1.191 +  all, with some notable exceptions: Output.output is required when
   1.192 +  bypassing the standard channels (writeln etc.), or in token
   1.193 +  translations to produce properly formatted results; Output.raw is
   1.194 +  required when capturing already output material that will eventually
   1.195 +  be presented to the user a second time.  For the default print mode,
   1.196 +  both Output.output and Output.raw have no effect.
   1.197 +
   1.198 +* Provers: Simplifier and Classical Reasoner now support proof context
   1.199 +  dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
   1.200 +  components are stored in the theory and patched into the
   1.201 +  simpset/claset when used in an Isar proof context.  Context
   1.202 +  dependent components are maintained by the following theory
   1.203 +  operations:
   1.204 +
   1.205 +    Simplifier.add_context_simprocs
   1.206 +    Simplifier.del_context_simprocs
   1.207 +    Simplifier.set_context_subgoaler
   1.208 +    Simplifier.reset_context_subgoaler
   1.209 +    Simplifier.add_context_looper
   1.210 +    Simplifier.del_context_looper
   1.211 +    Simplifier.add_context_unsafe_solver
   1.212 +    Simplifier.add_context_safe_solver
   1.213 +
   1.214 +    Classical.add_context_safe_wrapper
   1.215 +    Classical.del_context_safe_wrapper
   1.216 +    Classical.add_context_unsafe_wrapper
   1.217 +    Classical.del_context_unsafe_wrapper
   1.218 +
   1.219 +  IMPORTANT NOTE: proof tools (methods etc.) need to use
   1.220 +  local_simpset_of and local_claset_of to instead of the primitive
   1.221 +  Simplifier.get_local_simpset and Classical.get_local_claset,
   1.222 +  respectively, in order to see the context dependent fields!
   1.223 +
   1.224 +
   1.225  
   1.226  New in Isabelle2004 (April 2004)
   1.227  --------------------------------
     2.1 --- a/etc/isar-keywords.el	Wed Apr 13 09:48:41 2005 +0200
     2.2 +++ b/etc/isar-keywords.el	Wed Apr 13 18:34:22 2005 +0200
     2.3 @@ -7,7 +7,6 @@
     2.4  
     2.5  (defconst isar-keywords-major
     2.6    '("\\."
     2.7 -    "\\.\\."
     2.8      "ML"
     2.9      "ML_command"
    2.10      "ML_setup"
    2.11 @@ -19,6 +18,7 @@
    2.12      "ProofGeneral\\.restart"
    2.13      "ProofGeneral\\.try_context_thy_only"
    2.14      "ProofGeneral\\.undo"
    2.15 +    "\\.\\."
    2.16      "also"
    2.17      "apply"
    2.18      "apply_end"
    2.19 @@ -90,6 +90,7 @@
    2.20      "method_setup"
    2.21      "moreover"
    2.22      "next"
    2.23 +    "no_syntax"
    2.24      "nonterminals"
    2.25      "note"
    2.26      "obtain"
    2.27 @@ -362,6 +363,7 @@
    2.28      "local"
    2.29      "locale"
    2.30      "method_setup"
    2.31 +    "no_syntax"
    2.32      "nonterminals"
    2.33      "oracle"
    2.34      "parse_ast_translation"
     3.1 --- a/etc/settings	Wed Apr 13 09:48:41 2005 +0200
     3.2 +++ b/etc/settings	Wed Apr 13 18:34:22 2005 +0200
     3.3 @@ -145,6 +145,9 @@
     3.4  #Where to look for docs (multiple dirs separated by ':').
     3.5  ISABELLE_DOCS="$ISABELLE_HOME/doc"
     3.6  
     3.7 +#Preferred document format
     3.8 +ISABELLE_DOC_FORMAT=pdf
     3.9 +
    3.10  #The dvi file viewer
    3.11  DVI_VIEWER=xdvi
    3.12  #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
     4.1 --- a/lib/Tools/display	Wed Apr 13 09:48:41 2005 +0200
     4.2 +++ b/lib/Tools/display	Wed Apr 13 18:34:22 2005 +0200
     4.3 @@ -28,21 +28,6 @@
     4.4  }
     4.5  
     4.6  
     4.7 -function view()
     4.8 -{
     4.9 -  if [ "${1%%.dvi}.dvi" == "$1" ]; then
    4.10 -    exec $DVI_VIEWER "$1"
    4.11 -    return
    4.12 -  fi
    4.13 -
    4.14 -  if [ "${1%%.pdf}.pdf" == "$1" ]; then
    4.15 -    exec $PDF_VIEWER "$1"
    4.16 -    return
    4.17 -  fi
    4.18 -
    4.19 -  fail "Unknown file type: $FILE";
    4.20 -}
    4.21 -
    4.22  ## process command line
    4.23  
    4.24  # options
    4.25 @@ -75,11 +60,22 @@
    4.26  
    4.27  [ -f "$FILE" ] || fail "Bad file: $FILE"
    4.28  
    4.29 +case "$FILE" in
    4.30 +    *.dvi)
    4.31 +      VIEWER="$DVI_VIEWER"
    4.32 +      ;;
    4.33 +    *.pdf)
    4.34 +      VIEWER="$PDF_VIEWER"
    4.35 +      ;;
    4.36 +    *)
    4.37 +      fail "Unknown file type: $FILE";
    4.38 +esac
    4.39 +
    4.40  if [ -n "$CLEAN" ]; then
    4.41 -  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE")
    4.42 -  mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE"
    4.43 -  view "$PRIVATE_FILE"
    4.44 +  PRIVATE_FILE="$ISABELLE_TMP/$$"$(basename "$FILE")
    4.45 +  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    4.46 +  $VIEWER "$PRIVATE_FILE"
    4.47    rm -f "$PRIVATE_FILE"
    4.48  else
    4.49 -  view "$FILE"
    4.50 +  exec $VIEWER "$FILE"
    4.51  fi
     5.1 --- a/lib/Tools/doc	Wed Apr 13 09:48:41 2005 +0200
     5.2 +++ b/lib/Tools/doc	Wed Apr 13 18:34:22 2005 +0200
     5.3 @@ -40,6 +40,7 @@
     5.4    IFS=":"
     5.5    for DIR in $ISABELLE_DOCS
     5.6    do
     5.7 +    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
     5.8      [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
     5.9    done
    5.10    IFS="$ORIG_IFS"
    5.11 @@ -48,7 +49,12 @@
    5.12    IFS=":"
    5.13    for DIR in $ISABELLE_DOCS
    5.14    do
    5.15 -    [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
    5.16 +    IFS="$ORIG_IFS"
    5.17 +    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    5.18 +    for FMT in "$ISABELLE_DOC_FORMAT" dvi
    5.19 +    do
    5.20 +      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; }
    5.21 +    done
    5.22    done
    5.23    IFS="$ORIG_IFS"
    5.24    fail "Unknown Isabelle document: $DOC"  
     6.1 --- a/lib/Tools/mkdir	Wed Apr 13 09:48:41 2005 +0200
     6.2 +++ b/lib/Tools/mkdir	Wed Apr 13 18:34:22 2005 +0200
     6.3 @@ -137,7 +137,7 @@
     6.4      echo "OUT = \$(ISABELLE_OUTPUT)"
     6.5      echo "LOG = \$(OUT)/log"
     6.6      echo
     6.7 -    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d pdf  ## -D generated"
     6.8 +    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
     6.9      echo
    6.10      echo
    6.11      echo "## $NAME"
     7.1 --- a/src/HOL/Import/import_package.ML	Wed Apr 13 09:48:41 2005 +0200
     7.2 +++ b/src/HOL/Import/import_package.ML	Wed Apr 13 18:34:22 2005 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  
     7.5  signature IMPORT_PACKAGE =
     7.6  sig
     7.7 -    val import_meth: Args.src -> Proof.context -> Proof.method
     7.8 +    val import_meth: Method.src -> Proof.context -> Proof.method
     7.9      val setup      : (theory -> theory) list
    7.10      val debug      : bool ref
    7.11  end
     8.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Apr 13 09:48:41 2005 +0200
     8.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 13 18:34:22 2005 +0200
     8.3 @@ -51,8 +51,8 @@
     8.4         induction : thm,
     8.5         size : thm list,
     8.6         simps : thm list}
     8.7 -  val rep_datatype : string list option -> (thmref * Args.src list) list list ->
     8.8 -    (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory *
     8.9 +  val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
    8.10 +    (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> theory *
    8.11        {distinct : thm list list,
    8.12         inject : thm list list,
    8.13         exhaustion : thm list,
    8.14 @@ -244,7 +244,8 @@
    8.15  val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
    8.16  val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
    8.17  
    8.18 -val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
    8.19 +val varss =
    8.20 +  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
    8.21  
    8.22  val inst_tac = Method.bires_inst_tac false;
    8.23  
     9.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Apr 13 09:48:41 2005 +0200
     9.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 13 18:34:22 2005 +0200
     9.3 @@ -44,14 +44,14 @@
     9.4    val inductive_forall_name: string
     9.5    val inductive_forall_def: thm
     9.6    val rulify: thm -> thm
     9.7 -  val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
     9.8 +  val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
     9.9    val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
    9.10    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    9.11      ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    9.12        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    9.13         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    9.14    val add_inductive: bool -> bool -> string list ->
    9.15 -    ((bstring * string) * Args.src list) list -> (thmref * Args.src list) list ->
    9.16 +    ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list ->
    9.17      theory -> theory *
    9.18        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    9.19         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    10.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 13 09:48:41 2005 +0200
    10.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 13 18:34:22 2005 +0200
    10.3 @@ -466,13 +466,14 @@
    10.4    in 
    10.5      (add_ind_realizers (hd sets) (case arg of
    10.6          NONE => sets | SOME NONE => []
    10.7 -      | SOME (SOME sets') => sets \\ map (Sign.intern_const (sign_of thy)) sets')
    10.8 +      | SOME (SOME sets') => sets \\ sets')
    10.9        thy, thm)
   10.10    end;
   10.11  
   10.12 -val rlz_attrib_global = Attrib.syntax (Scan.lift
   10.13 -  (Scan.option (Args.$$$ "irrelevant" |--
   10.14 -    Scan.option (Args.colon |-- Scan.repeat1 Args.name))) >> rlz_attrib);
   10.15 +val rlz_attrib_global = Attrib.syntax
   10.16 + ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   10.17 +    Scan.option (Scan.lift (Args.colon) |--
   10.18 +      Scan.repeat1 Args.global_const))) >> rlz_attrib);
   10.19  
   10.20  val setup = [Attrib.add_attributes [("ind_realizer",
   10.21    (rlz_attrib_global, K Attrib.undef_local_attribute),
    11.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Apr 13 09:48:41 2005 +0200
    11.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 13 18:34:22 2005 +0200
    11.3 @@ -8,7 +8,7 @@
    11.4  signature PRIMREC_PACKAGE =
    11.5  sig
    11.6    val quiet_mode: bool ref
    11.7 -  val add_primrec: string -> ((bstring * string) * Args.src list) list
    11.8 +  val add_primrec: string -> ((bstring * string) * Attrib.src list) list
    11.9      -> theory -> theory * thm list
   11.10    val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
   11.11      -> theory -> theory * thm list
    12.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Apr 13 09:48:41 2005 +0200
    12.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Apr 13 18:34:22 2005 +0200
    12.3 @@ -23,19 +23,19 @@
    12.4    val cong_del_local: Proof.context attribute
    12.5    val wf_add_local: Proof.context attribute
    12.6    val wf_del_local: Proof.context attribute
    12.7 -  val add_recdef: bool -> xstring -> string -> ((bstring * string) * Args.src list) list ->
    12.8 -    Args.src option -> theory -> theory
    12.9 +  val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
   12.10 +    Attrib.src option -> theory -> theory
   12.11        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   12.12    val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
   12.13      theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   12.14 -  val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list ->
   12.15 +  val add_recdef_old: xstring -> string -> ((bstring * string) * Attrib.src list) list ->
   12.16      simpset * thm list -> theory ->
   12.17      theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   12.18 -  val defer_recdef: xstring -> string list -> (thmref * Args.src list) list
   12.19 +  val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
   12.20      -> theory -> theory * {induct_rules: thm}
   12.21    val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
   12.22      -> theory -> theory * {induct_rules: thm}
   12.23 -  val recdef_tc: bstring * Args.src list -> xstring -> int option
   12.24 +  val recdef_tc: bstring * Attrib.src list -> xstring -> int option
   12.25      -> bool -> theory -> ProofHistory.T
   12.26    val recdef_tc_i: bstring * theory attribute list -> string -> int option
   12.27      -> bool -> theory -> ProofHistory.T
    13.1 --- a/src/Provers/classical.ML	Wed Apr 13 09:48:41 2005 +0200
    13.2 +++ b/src/Provers/classical.ML	Wed Apr 13 18:34:22 2005 +0200
    13.3 @@ -168,8 +168,8 @@
    13.4    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    13.5    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
    13.6    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    13.7 -  val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
    13.8 -  val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    13.9 +  val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
   13.10 +  val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
   13.11    val setup: (theory -> theory) list
   13.12  
   13.13    val get_delta_claset: ProofContext.context -> claset
    14.1 --- a/src/Provers/induct_method.ML	Wed Apr 13 09:48:41 2005 +0200
    14.2 +++ b/src/Provers/induct_method.ML	Wed Apr 13 18:34:22 2005 +0200
    14.3 @@ -326,20 +326,14 @@
    14.4  
    14.5  local
    14.6  
    14.7 -fun check k get name =
    14.8 -  (case get name of SOME x => x
    14.9 -  | NONE => error ("No rule for " ^ k ^ " " ^ quote name));
   14.10 -
   14.11 -fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
   14.12 +fun named_rule k arg get =
   14.13 +  Scan.lift (Args.$$$ k -- Args.colon) |-- arg :-- (fn name => Scan.peek (fn ctxt =>
   14.14 +    (case get ctxt name of SOME x => Scan.succeed x
   14.15 +    | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))) >> #2;
   14.16  
   14.17  fun rule get_type get_set =
   14.18 -  Scan.depend (fn ctxt =>
   14.19 -    let val sg = ProofContext.sign_of ctxt in
   14.20 -      spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
   14.21 -        Sign.certify_tyname sg o Sign.intern_tycon sg) ||
   14.22 -      spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
   14.23 -        Sign.certify_const sg o Sign.intern_const sg)
   14.24 -    end >> pair ctxt) ||
   14.25 +  named_rule InductAttrib.typeN Args.local_tyname get_type ||
   14.26 +  named_rule InductAttrib.setN Args.local_const get_set ||
   14.27    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
   14.28  
   14.29  val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
    15.1 --- a/src/Pure/Isar/ROOT.ML	Wed Apr 13 09:48:41 2005 +0200
    15.2 +++ b/src/Pure/Isar/ROOT.ML	Wed Apr 13 18:34:22 2005 +0200
    15.3 @@ -13,11 +13,11 @@
    15.4  use "proof_data.ML";
    15.5  use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*)
    15.6  use "context_rules.ML";
    15.7 +use "args.ML";
    15.8 +use "attrib.ML";
    15.9  use "locale.ML";
   15.10  use "proof.ML";
   15.11  use "proof_history.ML";
   15.12 -use "args.ML";
   15.13 -use "attrib.ML";
   15.14  use "net_rules.ML";
   15.15  use "induct_attrib.ML";
   15.16  use "method.ML";
   15.17 @@ -54,13 +54,16 @@
   15.18  struct
   15.19    structure ObjectLogic = ObjectLogic;
   15.20    structure AutoBind = AutoBind;
   15.21 +  structure RuleCases = RuleCases;
   15.22    structure ProofContext = ProofContext;
   15.23 +  structure ContextRules = ContextRules;
   15.24 +  structure Args = Args;
   15.25 +  structure Attrib = Attrib;
   15.26    structure Locale = Locale;
   15.27    structure Proof = Proof;
   15.28    structure ProofHistory = ProofHistory;
   15.29 -  structure Args = Args;
   15.30 -  structure Attrib = Attrib;
   15.31 -  structure ContextRules = ContextRules;
   15.32 +  structure NetRules = NetRules;
   15.33 +  structure InductAttrib = InductAttrib;
   15.34    structure Method = Method;
   15.35    structure Calculation = Calculation;
   15.36    structure Obtain = Obtain;
    16.1 --- a/src/Pure/Isar/args.ML	Wed Apr 13 09:48:41 2005 +0200
    16.2 +++ b/src/Pure/Isar/args.ML	Wed Apr 13 18:34:22 2005 +0200
    16.3 @@ -2,21 +2,35 @@
    16.4      ID:         $Id$
    16.5      Author:     Markus Wenzel, TU Muenchen
    16.6  
    16.7 -Concrete argument syntax (of attributes and methods).
    16.8 +Concrete argument syntax of attributes, methods etc. -- with special
    16.9 +support for embedded values and static binding.
   16.10  *)
   16.11  
   16.12  signature ARGS =
   16.13  sig
   16.14 +  datatype value = Name of string | Typ of typ | Term of term | Fact of thm list |
   16.15 +    Attribute of theory attribute * ProofContext.context attribute
   16.16    type T
   16.17 -  val val_of: T -> string
   16.18 -  val pos_of: T -> Position.T
   16.19 -  val str_of: T -> string
   16.20    val string_of: T -> string
   16.21 -  val ident: string * Position.T -> T
   16.22 -  val string: string * Position.T -> T
   16.23 -  val keyword: string * Position.T -> T
   16.24 +  val mk_ident: string * Position.T -> T
   16.25 +  val mk_string: string * Position.T -> T
   16.26 +  val mk_keyword: string * Position.T -> T
   16.27 +  val mk_name: string -> T
   16.28 +  val mk_typ: typ -> T
   16.29 +  val mk_term: term -> T
   16.30 +  val mk_fact: thm list -> T
   16.31 +  val mk_attribute: theory attribute * ProofContext.context attribute -> T
   16.32    val stopper: T * (T -> bool)
   16.33    val not_eof: T -> bool
   16.34 +  type src
   16.35 +  val src: (string * T list) * Position.T -> src
   16.36 +  val dest_src: src -> (string * T list) * Position.T
   16.37 +  val map_name: (string -> string) -> src -> src
   16.38 +  val map_values: (string -> string) -> (typ -> typ) -> (term -> term) -> (thm -> thm)
   16.39 +    -> src -> src
   16.40 +  val assignable: src -> src
   16.41 +  val assign: value option -> T -> unit
   16.42 +  val closure: src -> src
   16.43    val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
   16.44    val !!! : (T list -> 'a) -> T list -> 'a
   16.45    val $$$ : string -> T list -> string * T list
   16.46 @@ -30,15 +44,28 @@
   16.47    val parens: (T list -> 'a * T list) -> T list -> 'a * T list
   16.48    val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
   16.49    val mode: string -> 'a * T list -> bool * ('a * T list)
   16.50 +  val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
   16.51    val name: T list -> string * T list
   16.52 -  val name_dummy: T list -> string option * T list
   16.53    val nat: T list -> int * T list
   16.54    val int: T list -> int * T list
   16.55    val var: T list -> indexname * T list
   16.56 +  val list: (T list -> 'a * T list) -> T list -> 'a list * T list
   16.57 +  val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
   16.58    val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   16.59    val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   16.60    val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   16.61    val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   16.62 +  val ahead: T list -> T * T list
   16.63 +  val internal_name: T list -> string * T list
   16.64 +  val internal_typ: T list -> typ * T list
   16.65 +  val internal_term: T list -> term * T list
   16.66 +  val internal_fact: T list -> thm list * T list
   16.67 +  val internal_attribute: T list ->
   16.68 +    (theory attribute * ProofContext.context attribute) * T list
   16.69 +  val named_name: (string -> string) -> T list -> string * T list
   16.70 +  val named_typ: (string -> typ) -> T list -> typ * T list
   16.71 +  val named_term: (string -> term) -> T list -> term * T list
   16.72 +  val named_fact: (string -> thm list) -> T list -> thm list * T list
   16.73    val global_typ_raw: theory * T list -> typ * (theory * T list)
   16.74    val global_typ: theory * T list -> typ * (theory * T list)
   16.75    val global_term: theory * T list -> term * (theory * T list)
   16.76 @@ -47,15 +74,19 @@
   16.77    val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list)
   16.78    val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list)
   16.79    val local_prop: ProofContext.context * T list -> term * (ProofContext.context * T list)
   16.80 +  val global_tyname: theory * T list -> string * (theory * T list)
   16.81 +  val global_const: theory * T list -> string * (theory * T list)
   16.82 +  val local_tyname: ProofContext.context * T list -> string * (ProofContext.context * T list)
   16.83 +  val local_const: ProofContext.context * T list -> string * (ProofContext.context * T list)
   16.84 +  val thm_sel: T list -> PureThy.interval list * T list
   16.85    val bang_facts: ProofContext.context * T list -> thm list * (ProofContext.context * T list)
   16.86    val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
   16.87      -> ((int -> tactic) -> tactic) * ('a * T list)
   16.88 -  type src
   16.89 -  val src: (string * T list) * Position.T -> src
   16.90 -  val dest_src: src -> (string * T list) * Position.T
   16.91 -  val attribs: T list -> src list * T list
   16.92 -  val opt_attribs: T list -> src list * T list
   16.93 +  val attribs: (string -> string) -> T list -> src list * T list
   16.94 +  val opt_attribs: (string -> string) -> T list -> src list * T list
   16.95    val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
   16.96 +  val pretty_src: ProofContext.context -> src -> Pretty.T
   16.97 +  val pretty_attribs: ProofContext.context -> src list -> Pretty.T list
   16.98  end;
   16.99  
  16.100  structure Args: ARGS =
  16.101 @@ -64,33 +95,58 @@
  16.102  
  16.103  (** datatype T **)
  16.104  
  16.105 +(*An argument token is a symbol (with raw string value), together with
  16.106 +  an optional assigned internal value.  Note that an assignable ref
  16.107 +  designates an intermediate state of internalization -- it is NOT
  16.108 +  meant to persist.*)
  16.109 +
  16.110  datatype kind = Ident | String | Keyword | EOF;
  16.111 -datatype T = Arg of kind * (string * Position.T);
  16.112 +
  16.113 +type symbol = kind * string * Position.T;
  16.114  
  16.115 -fun val_of (Arg (_, (x, _))) = x;
  16.116 -fun pos_of (Arg (_, (_, pos))) = pos;
  16.117 +datatype value =
  16.118 +  Name of string |
  16.119 +  Typ of typ |
  16.120 +  Term of term |
  16.121 +  Fact of thm list |
  16.122 +  Attribute of theory attribute * ProofContext.context attribute;
  16.123 +
  16.124 +datatype slot =
  16.125 +  Empty |
  16.126 +  Value of value option |
  16.127 +  Assignable of value option ref;
  16.128 +
  16.129 +datatype T = Arg of symbol * slot;
  16.130  
  16.131 -fun str_of (Arg (Ident, (x, _))) = x
  16.132 -  | str_of (Arg (String, (x, _))) = Library.quote x
  16.133 -  | str_of (Arg (Keyword, (x, _))) = x
  16.134 -  | str_of (Arg (EOF, _)) = "end-of-text";
  16.135 +fun string_of (Arg ((Ident, x, _), _)) = x
  16.136 +  | string_of (Arg ((String, x, _), _)) = Library.quote x
  16.137 +  | string_of (Arg ((Keyword, x, _), _)) = x
  16.138 +  | string_of (Arg ((EOF, _, _), _)) = "";
  16.139 +
  16.140 +fun sym_of (Arg ((_, x, _), _)) = x;
  16.141 +fun pos_of (Arg ((_, _, pos), _)) = pos;
  16.142 +
  16.143 +
  16.144 +(* basic constructors *)
  16.145  
  16.146 -fun string_of (Arg (Ident, (x, _))) = x
  16.147 -  | string_of (Arg (String, (x, _))) = Library.quote x
  16.148 -  | string_of (Arg (Keyword, (x, _))) = x
  16.149 -  | string_of (Arg (EOF, _)) = "";
  16.150 +fun mk_symbol k (x, p) = Arg ((k, x, p), Empty);
  16.151 +fun mk_value k v = Arg ((Keyword, k, Position.none), Value (SOME v));
  16.152  
  16.153 -fun arg kind x_pos = Arg (kind, x_pos);
  16.154 -val ident = arg Ident;
  16.155 -val string = arg String;
  16.156 -val keyword = arg Keyword;
  16.157 +val mk_ident = mk_symbol Ident;
  16.158 +val mk_string = mk_symbol String;
  16.159 +val mk_keyword = mk_symbol Keyword;
  16.160 +val mk_name = mk_value "<name>" o Name;
  16.161 +val mk_typ = mk_value "<typ>" o Typ;
  16.162 +val mk_term = mk_value "<term>" o Term;
  16.163 +val mk_fact = mk_value "<fact>" o Fact;
  16.164 +val mk_attribute = mk_value "<attribute>" o Attribute;
  16.165  
  16.166  
  16.167  (* eof *)
  16.168  
  16.169 -val eof = arg EOF ("", Position.none);
  16.170 +val eof = mk_symbol EOF ("", Position.none);
  16.171  
  16.172 -fun is_eof (Arg (EOF, _)) = true
  16.173 +fun is_eof (Arg ((EOF, _, _), _)) = true
  16.174    | is_eof _ = false;
  16.175  
  16.176  val stopper = (eof, is_eof);
  16.177 @@ -98,11 +154,55 @@
  16.178  
  16.179  
  16.180  
  16.181 +(** datatype src **)
  16.182 +
  16.183 +datatype src = Src of (string * T list) * Position.T;
  16.184 +
  16.185 +val src = Src;
  16.186 +fun dest_src (Src src) = src;
  16.187 +
  16.188 +fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
  16.189 +fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
  16.190 +
  16.191 +
  16.192 +(* values *)
  16.193 +
  16.194 +fun map_value f (Arg (s, Value (SOME v))) = Arg (s, Value (SOME (f v)))
  16.195 +  | map_value _ arg = arg;
  16.196 +
  16.197 +fun map_values f g h i = map_args (map_value
  16.198 +  (fn Name s => Name (f s)
  16.199 +    | Typ T => Typ (g T)
  16.200 +    | Term t => Term (h t)
  16.201 +    | Fact ths => Fact (map i ths)
  16.202 +    | Attribute att => Attribute att));
  16.203 +
  16.204 +
  16.205 +(* static binding *)
  16.206 +
  16.207 +(*1st stage: make empty slots assignable*)
  16.208 +val assignable =
  16.209 +  map_args (fn Arg (s, Empty) => Arg (s, Assignable (ref NONE)) | arg => arg);
  16.210 +
  16.211 +(*2nd stage: assign values as side-effect of scanning*)
  16.212 +fun assign v (arg as Arg (_, Assignable r)) = r := v
  16.213 +  | assign _ _ = ();
  16.214 +
  16.215 +val ahead = Scan.ahead (Scan.one not_eof);
  16.216 +fun touch scan = ahead -- scan >> (fn (arg, y) => (assign NONE arg; y));
  16.217 +
  16.218 +(*3rd stage: static closure of final values*)
  16.219 +val closure =
  16.220 +  map_args (fn Arg (s, Assignable (ref v)) => Arg (s, Value v) | arg => arg);
  16.221 +
  16.222 +
  16.223 +
  16.224  (** scanners **)
  16.225  
  16.226  (* position *)
  16.227  
  16.228 -fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
  16.229 +fun position scan =
  16.230 +  (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
  16.231  
  16.232  
  16.233  (* cut *)
  16.234 @@ -110,7 +210,7 @@
  16.235  fun !!! scan =
  16.236    let
  16.237      fun get_pos [] = " (past end-of-text!)"
  16.238 -      | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
  16.239 +      | get_pos (arg :: _) = Position.str_of (pos_of arg);
  16.240  
  16.241      fun err (args, NONE) = "Argument syntax error" ^ get_pos args
  16.242        | err (args, SOME msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
  16.243 @@ -119,8 +219,20 @@
  16.244  
  16.245  (* basic *)
  16.246  
  16.247 -fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
  16.248 -fun $$$ x = $$$$ x >> val_of;
  16.249 +fun some_ident f =
  16.250 +  touch (Scan.some (fn Arg ((Ident, x, _), _) => f x | _ => NONE));
  16.251 +
  16.252 +val named =
  16.253 +  touch (Scan.one (fn Arg ((k, _, _), _) => k = Ident orelse k = String));
  16.254 +
  16.255 +val symbolic =
  16.256 +  touch (Scan.one (fn Arg ((k, x, _), _) => k = Keyword andalso OuterLex.is_sid x));
  16.257 +
  16.258 +fun &&& x =
  16.259 +  touch (Scan.one (fn Arg ((k, y, _), _) => k = Keyword andalso x = y));
  16.260 +
  16.261 +fun $$$ x =
  16.262 +  touch (Scan.one (fn Arg ((k, y, _), _) => (k = Ident orelse k = Keyword) andalso x = y) >> sym_of);
  16.263  
  16.264  val add = $$$ "add";
  16.265  val del = $$$ "del";
  16.266 @@ -132,31 +244,24 @@
  16.267  
  16.268  fun parens scan = $$$ "(" |-- scan --| $$$ ")";
  16.269  fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
  16.270 -fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
  16.271 -
  16.272 -val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
  16.273 -val name_dummy = $$$ "_" >> K NONE || name >> SOME;
  16.274 +fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
  16.275 +fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
  16.276  
  16.277 -val keyword_symid =
  16.278 -  Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
  16.279 +val name = named >> sym_of;
  16.280  
  16.281 -fun kind f = Scan.one (K true) :--
  16.282 -  (fn Arg (Ident, (x, _)) =>
  16.283 -    (case f x of SOME y => Scan.succeed y | _ => Scan.fail)
  16.284 -  | _ => Scan.fail) >> #2;
  16.285 -
  16.286 -val nat = kind Syntax.read_nat;
  16.287 +val nat = some_ident Syntax.read_nat;
  16.288  val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
  16.289  
  16.290 -(*read variable name; leading '?' may be omitted if name contains no dot*)
  16.291 -val var = kind (Option.map #1 o (fn s =>
  16.292 -  SOME (Term.dest_Var (Syntax.read_var s))
  16.293 -    handle _ => SOME (Term.dest_Var (Syntax.read_var ("?" ^ s)))
  16.294 -    handle _ => NONE));
  16.295 +(*variable name; leading '?' may be omitted if name contains no dot*)
  16.296 +val read_var = try (#1 o Term.dest_Var o Syntax.read_var);
  16.297 +val var = some_ident read_var || some_ident (fn x => read_var ("?" ^ x));
  16.298  
  16.299  
  16.300  (* enumerations *)
  16.301  
  16.302 +fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
  16.303 +fun list scan = list1 scan || Scan.succeed [];
  16.304 +
  16.305  fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
  16.306  fun enum sep scan = enum1 sep scan || Scan.succeed [];
  16.307  
  16.308 @@ -164,25 +269,60 @@
  16.309  fun and_list scan = enum "and" scan;
  16.310  
  16.311  
  16.312 +(* values *)
  16.313 +
  16.314 +fun value dest = Scan.some  (*no touch here*)
  16.315 +  (fn Arg (_, Value (SOME v)) => (SOME (dest v) handle Match => NONE)
  16.316 +    | Arg _ => NONE);
  16.317 +
  16.318 +fun evaluate mk eval arg =
  16.319 +  let val x = eval (sym_of arg) in (assign (SOME (mk x)) arg; x) end;
  16.320 +
  16.321 +val internal_name = value (fn Name s => s);
  16.322 +val internal_typ = value (fn Typ T => T);
  16.323 +val internal_term = value (fn Term t => t);
  16.324 +val internal_fact = value (fn Fact ths => ths);
  16.325 +val internal_attribute = value (fn Attribute att => att);
  16.326 +
  16.327 +fun named_name intern = internal_name || named >> evaluate Name intern;
  16.328 +fun named_typ readT = internal_typ || named >> evaluate Typ readT;
  16.329 +fun named_term read = internal_term || named >> evaluate Term read;
  16.330 +fun named_fact get = internal_fact || named >> evaluate Fact get;
  16.331 +
  16.332 +
  16.333  (* terms and types *)
  16.334  
  16.335 -fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
  16.336 +val global_typ_raw = Scan.peek (named_typ o ProofContext.read_typ_raw o ProofContext.init);
  16.337 +val global_typ = Scan.peek (named_typ o ProofContext.read_typ o ProofContext.init);
  16.338 +val global_term = Scan.peek (named_term o ProofContext.read_term o ProofContext.init);
  16.339 +val global_prop = Scan.peek (named_term o ProofContext.read_prop o ProofContext.init);
  16.340  
  16.341 -val global_typ_raw = gen_item (ProofContext.read_typ_raw o ProofContext.init);
  16.342 -val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
  16.343 -val global_term = gen_item (ProofContext.read_term o ProofContext.init);
  16.344 -val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
  16.345 -
  16.346 -val local_typ_raw = gen_item ProofContext.read_typ_raw;
  16.347 -val local_typ = gen_item ProofContext.read_typ;
  16.348 -val local_term = gen_item ProofContext.read_term;
  16.349 -val local_prop = gen_item ProofContext.read_prop;
  16.350 +val local_typ_raw = Scan.peek (named_typ o ProofContext.read_typ_raw);
  16.351 +val local_typ = Scan.peek (named_typ o ProofContext.read_typ);
  16.352 +val local_term = Scan.peek (named_term o ProofContext.read_term);
  16.353 +val local_prop = Scan.peek (named_term o ProofContext.read_prop);
  16.354  
  16.355  
  16.356 -(* bang facts *)
  16.357 +(* type and constant names *)
  16.358 +
  16.359 +val dest_tyname = fn Type (c, _) => c | TFree (a, _) => a | _ => "";
  16.360 +val dest_const = fn Const (c, _) => c | Free (x, _) => x | _ => "";
  16.361 +
  16.362 +val global_tyname = Scan.peek (named_typ o Sign.read_tyname o Theory.sign_of) >> dest_tyname;
  16.363 +val global_const = Scan.peek (named_term o Sign.read_const o Theory.sign_of) >> dest_const;
  16.364 +val local_tyname = Scan.peek (named_typ o ProofContext.read_tyname) >> dest_tyname;
  16.365 +val local_const = Scan.peek (named_term o ProofContext.read_const) >> dest_const;
  16.366  
  16.367 -val bang_facts = Scan.depend (fn ctxt =>
  16.368 -  ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
  16.369 +
  16.370 +(* misc *)
  16.371 +
  16.372 +val thm_sel = parens (list1
  16.373 + (nat --| $$$ "-" -- nat >> PureThy.FromTo ||
  16.374 +  nat --| $$$ "-" >> PureThy.From ||
  16.375 +  nat >> PureThy.Single));
  16.376 +
  16.377 +val bang_facts = Scan.peek (fn ctxt =>
  16.378 +  $$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []);
  16.379  
  16.380  
  16.381  (* goal specification *)
  16.382 @@ -190,62 +330,72 @@
  16.383  (* range *)
  16.384  
  16.385  val from_to =
  16.386 -  nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
  16.387 -  nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
  16.388 +  nat -- ($$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
  16.389 +  nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
  16.390    nat >> (fn i => fn tac => tac i) ||
  16.391 -  $$$$ "!" >> K ALLGOALS;
  16.392 +  $$$ "!" >> K ALLGOALS;
  16.393  
  16.394 -val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
  16.395 +val goal = $$$ "[" |-- !!! (from_to --| $$$ "]");
  16.396  fun goal_spec def = Scan.lift (Scan.optional goal def);
  16.397  
  16.398  
  16.399 -(* args *)
  16.400 +
  16.401 +(* attribs *)
  16.402 +
  16.403 +local
  16.404  
  16.405  val exclude = explode "()[],";
  16.406  
  16.407 -fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
  16.408 -  k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
  16.409 -
  16.410 -fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
  16.411 -  >> (fn (x, (ys, z)) => x :: ys @ [z]);
  16.412 +fun atomic blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
  16.413 +    k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ","));
  16.414  
  16.415  fun args blk x = Scan.optional (args1 blk) [] x
  16.416  and args1 blk x =
  16.417    ((Scan.repeat1
  16.418 -    (Scan.repeat1 (atom_arg blk) ||
  16.419 -      paren_args "(" ")" args ||
  16.420 -      paren_args "[" "]" args)) >> List.concat) x;
  16.421 +    (Scan.repeat1 (atomic blk) ||
  16.422 +      argsp "(" ")" ||
  16.423 +      argsp "[" "]")) >> List.concat) x
  16.424 +and argsp l r x =
  16.425 +  (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x;
  16.426 +
  16.427 +in
  16.428  
  16.429 +fun attribs intern =
  16.430 +  let
  16.431 +    val attrib_name = internal_name || (symbolic || named) >> evaluate Name intern;
  16.432 +    val attrib = position (attrib_name -- !!! (args false)) >> src;
  16.433 +  in $$$ "[" |-- !!! (list attrib --| $$$ "]") end;
  16.434 +
  16.435 +fun opt_attribs intern = Scan.optional (attribs intern) [];
  16.436 +
  16.437 +end;
  16.438  
  16.439  
  16.440 -(** type src **)
  16.441 -
  16.442 -datatype src = Src of (string * T list) * Position.T;
  16.443 -
  16.444 -val src = Src;
  16.445 -fun dest_src (Src src) = src;
  16.446 -
  16.447 -fun err_in_src kind msg (Src ((s, args), pos)) =
  16.448 -  error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
  16.449 -    space_implode " " (map str_of args));
  16.450 -    
  16.451 -
  16.452 -(* argument syntax *)
  16.453 +(* syntax interface *)
  16.454  
  16.455  fun syntax kind scan (src as Src ((s, args), pos)) st =
  16.456    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
  16.457      (SOME x, (st', [])) => (st', x)
  16.458 -  | (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos)));
  16.459 +  | (_, (_, args')) =>
  16.460 +      error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
  16.461 +        space_implode " " (map string_of args')));
  16.462 +
  16.463  
  16.464  
  16.465 -(* attribs *)
  16.466 -
  16.467 -fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
  16.468 -fun list scan = list1 scan || Scan.succeed [];
  16.469 +(** pretty printing **)
  16.470  
  16.471 -val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
  16.472 -val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
  16.473 -val opt_attribs = Scan.optional attribs [];
  16.474 +fun pretty_src ctxt src =
  16.475 +  let
  16.476 +    fun prt (Arg (_, Value (SOME (Name s)))) = Pretty.str (quote s)
  16.477 +      | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
  16.478 +      | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
  16.479 +      | prt (Arg (_, Value (SOME (Fact ths)))) = ProofContext.pretty_thms ctxt ths
  16.480 +      | prt arg = Pretty.str (string_of arg);
  16.481 +    val (s, args) = #1 (dest_src src);
  16.482 +  in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
  16.483  
  16.484 +fun pretty_attribs _ [] = []
  16.485 +  | pretty_attribs ctxt srcs =
  16.486 +      [Pretty.enclose "[" "]" (Pretty.commas (map (pretty_src ctxt) srcs))];
  16.487  
  16.488  end;
    17.1 --- a/src/Pure/Isar/attrib.ML	Wed Apr 13 09:48:41 2005 +0200
    17.2 +++ b/src/Pure/Isar/attrib.ML	Wed Apr 13 18:34:22 2005 +0200
    17.3 @@ -8,37 +8,46 @@
    17.4  signature BASIC_ATTRIB =
    17.5  sig
    17.6    val print_attributes: theory -> unit
    17.7 -  val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> Proof.context attribute)
    17.8 +  val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute)
    17.9      -> string -> unit
   17.10  end;
   17.11  
   17.12  signature ATTRIB =
   17.13  sig
   17.14    include BASIC_ATTRIB
   17.15 +  type src
   17.16    exception ATTRIB_FAIL of (string * Position.T) * exn
   17.17 -  val global_attribute: theory -> Args.src -> theory attribute
   17.18 -  val local_attribute: theory -> Args.src -> Proof.context attribute
   17.19 -  val multi_attribute: theory -> Args.src -> Locale.multi_attribute
   17.20 -  val local_attribute': Proof.context -> Args.src -> Proof.context attribute
   17.21 +  val intern: Sign.sg -> xstring -> string
   17.22 +  val intern_src: Sign.sg -> src -> src
   17.23 +  val global_attribute_i: theory -> src -> theory attribute
   17.24 +  val global_attribute: theory -> src -> theory attribute
   17.25 +  val local_attribute_i: theory -> src -> ProofContext.context attribute
   17.26 +  val local_attribute: theory -> src -> ProofContext.context attribute
   17.27 +  val context_attribute_i: ProofContext.context -> Args.src -> ProofContext.context attribute
   17.28 +  val context_attribute: ProofContext.context -> Args.src -> ProofContext.context attribute
   17.29    val undef_global_attribute: theory attribute
   17.30 -  val undef_local_attribute: Proof.context attribute
   17.31 -  val add_attributes: (bstring * ((Args.src -> theory attribute) *
   17.32 -      (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
   17.33 +  val undef_local_attribute: ProofContext.context attribute
   17.34 +  val crude_closure: ProofContext.context -> src -> src
   17.35 +  val add_attributes: (bstring * ((src -> theory attribute) *
   17.36 +      (src -> ProofContext.context attribute)) * string) list -> theory -> theory
   17.37    val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
   17.38    val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
   17.39    val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
   17.40 -  val local_thm: Proof.context * Args.T list -> thm * (Proof.context * Args.T list)
   17.41 -  val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
   17.42 -  val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
   17.43 -  val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
   17.44 -  val no_args: 'a attribute -> Args.src -> 'a attribute
   17.45 -  val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
   17.46 +  val local_thm: ProofContext.context * Args.T list -> thm * (ProofContext.context * Args.T list)
   17.47 +  val local_thms: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
   17.48 +  val local_thmss: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
   17.49 +  val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
   17.50 +  val no_args: 'a attribute -> src -> 'a attribute
   17.51 +  val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
   17.52 +  val attribute: (theory attribute * ProofContext.context attribute) -> src
   17.53    val setup: (theory -> theory) list
   17.54  end;
   17.55  
   17.56  structure Attrib: ATTRIB =
   17.57  struct
   17.58  
   17.59 +type src = Args.src;
   17.60 +
   17.61  
   17.62  (** attributes theory data **)
   17.63  
   17.64 @@ -50,7 +59,7 @@
   17.65    type T =
   17.66      {space: NameSpace.T,
   17.67       attrs:
   17.68 -       ((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute))
   17.69 +       ((((src -> theory attribute) * (src -> ProofContext.context attribute))
   17.70           * string) * stamp) Symtab.table};
   17.71  
   17.72    val empty = {space = NameSpace.empty, attrs = Symtab.empty};
   17.73 @@ -76,18 +85,23 @@
   17.74  val print_attributes = AttributesData.print;
   17.75  
   17.76  
   17.77 +(* interning *)
   17.78 +
   17.79 +val intern = NameSpace.intern o #space o AttributesData.get_sg;
   17.80 +val intern_src = Args.map_name o intern;
   17.81 +
   17.82 +
   17.83  (* get global / local attributes *)
   17.84  
   17.85  exception ATTRIB_FAIL of (string * Position.T) * exn;
   17.86  
   17.87  fun gen_attribute which thy =
   17.88    let
   17.89 -    val {space, attrs} = AttributesData.get thy;
   17.90 +    val {attrs, ...} = AttributesData.get thy;
   17.91  
   17.92      fun attr src =
   17.93        let
   17.94 -        val ((raw_name, _), pos) = Args.dest_src src;
   17.95 -        val name = NameSpace.intern space raw_name;
   17.96 +        val ((name, _), pos) = Args.dest_src src;
   17.97        in
   17.98          (case Symtab.lookup (attrs, name) of
   17.99            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
  17.100 @@ -95,19 +109,33 @@
  17.101        end;
  17.102    in attr end;
  17.103  
  17.104 -val global_attribute = gen_attribute fst;
  17.105 -val local_attribute = gen_attribute snd;
  17.106 -fun multi_attribute thy src =
  17.107 -      (global_attribute thy src, local_attribute thy src);
  17.108 -val local_attribute' = local_attribute o ProofContext.theory_of;
  17.109 +val global_attribute_i = gen_attribute fst;
  17.110 +fun global_attribute thy = global_attribute_i thy o intern_src (Theory.sign_of thy);
  17.111 +
  17.112 +val local_attribute_i = gen_attribute snd;
  17.113 +fun local_attribute thy = local_attribute_i thy o intern_src (Theory.sign_of thy);
  17.114 +
  17.115 +val context_attribute_i = local_attribute_i o ProofContext.theory_of;
  17.116 +val context_attribute = local_attribute o ProofContext.theory_of;
  17.117  
  17.118  val undef_global_attribute: theory attribute =
  17.119    fn _ => error "attribute undefined in theory context";
  17.120  
  17.121 -val undef_local_attribute: Proof.context attribute =
  17.122 +val undef_local_attribute: ProofContext.context attribute =
  17.123    fn _ => error "attribute undefined in proof context";
  17.124  
  17.125  
  17.126 +(* crude_closure *)
  17.127 +
  17.128 +(*Produce closure without knowing facts in advance! The following
  17.129 +  should work reasonably well for attribute parsers that do not peek
  17.130 +  at the thm structure.*)
  17.131 +
  17.132 +fun crude_closure ctxt src =
  17.133 + (try (transform_error (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl))) ();
  17.134 +  Args.closure src);
  17.135 +
  17.136 +
  17.137  (* add_attributes *)
  17.138  
  17.139  fun add_attributes raw_attrs thy =
  17.140 @@ -136,20 +164,24 @@
  17.141  
  17.142  (* theorems *)
  17.143  
  17.144 -val thm_sel = Args.parens (Scan.pass () (Args.enum1 "," (Scan.lift
  17.145 -  (   Args.nat --| Args.$$$ "-" -- Args.nat >> op upto
  17.146 -   || Args.nat >> single)) >> List.concat));
  17.147 +fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
  17.148 +  Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
  17.149 +  Scan.option Args.thm_sel -- Args.opt_attribs (intern (Theory.sign_of (theory_of st)))
  17.150 +  >> (fn (((name, fact), sel), srcs) =>
  17.151 +    let
  17.152 +      val ths = PureThy.select_thm (name, sel) fact;
  17.153 +      val atts = map (attrib (theory_of st)) srcs;
  17.154 +      val (st', ths') = Thm.applys_attributes ((st, ths), atts);
  17.155 +    in (st', pick name ths') end));
  17.156  
  17.157 -fun gen_thm get attrib app =
  17.158 -  Scan.depend (fn st => Args.name -- Scan.option thm_sel -- Args.opt_attribs >>
  17.159 -    (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs)));
  17.160 -
  17.161 -val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes;
  17.162 -val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes;
  17.163 +val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm;
  17.164 +val global_thms = gen_thm I global_attribute_i PureThy.get_thms (K I);
  17.165  val global_thmss = Scan.repeat global_thms >> List.concat;
  17.166  
  17.167 -val local_thm = gen_thm ProofContext.get_thm local_attribute' Thm.apply_attributes;
  17.168 -val local_thms = gen_thm ProofContext.get_thms local_attribute' Thm.applys_attributes;
  17.169 +val local_thm =
  17.170 +  gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms PureThy.single_thm;
  17.171 +val local_thms =
  17.172 +  gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms (K I);
  17.173  val local_thmss = Scan.repeat local_thms >> List.concat;
  17.174  
  17.175  
  17.176 @@ -201,119 +233,186 @@
  17.177  val OF_local = syntax (local_thmss >> apply);
  17.178  
  17.179  
  17.180 -(* where *)
  17.181 +(* read_instantiate: named instantiation of type and term variables *)
  17.182  
  17.183 -(*named instantiations; permits instantiation of type and term variables*)
  17.184 +local
  17.185  
  17.186 -fun read_instantiate _ [] _ thm = thm
  17.187 -  | read_instantiate context_of insts x thm =
  17.188 -      let
  17.189 -        val ctxt = context_of x;
  17.190 -        val sign = ProofContext.sign_of ctxt;
  17.191 +fun is_tvar (x, _) = (case Symbol.explode x of "'" :: _ => true | _ => false);
  17.192 +
  17.193 +fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
  17.194 +
  17.195 +fun the_sort sorts xi = valOf (sorts xi)
  17.196 +  handle Option.Option => error_var "No such type variable in theorem: " xi;
  17.197  
  17.198 -        (* Separate type and term insts,
  17.199 -           type insts must occur strictly before term insts *)
  17.200 -        fun has_type_var ((x, _), _) = (case Symbol.explode x of
  17.201 -             "'"::cs => true | cs => false);
  17.202 -        val (Tinst, tinsts) = take_prefix has_type_var insts;
  17.203 -        val _ = if exists has_type_var tinsts
  17.204 -              then error
  17.205 -                "Type instantiations must occur before term instantiations."
  17.206 -              else ();
  17.207 +fun the_type types xi = valOf (types xi)
  17.208 +  handle Option.Option => error_var "No such variable in theorem: " xi;
  17.209  
  17.210 -        val Tinsts = List.filter has_type_var insts;
  17.211 -        val tinsts = filter_out has_type_var insts;
  17.212 +fun unify_types sign types ((unifier, maxidx), (xi, u)) =
  17.213 +  let
  17.214 +    val T = the_type types xi;
  17.215 +    val U = Term.fastype_of u;
  17.216 +    val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
  17.217 +  in
  17.218 +    Type.unify (Sign.tsig_of sign) (unifier, maxidx') (T, U)
  17.219 +      handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
  17.220 +  end;
  17.221 +
  17.222 +fun typ_subst env = apsnd (Term.typ_subst_TVars env);
  17.223 +fun subst env = apsnd (Term.subst_TVars env);
  17.224  
  17.225 -        (* Type instantiations first *)
  17.226 -        (* Process type insts: Tinsts_env *)
  17.227 -        fun absent xi = error
  17.228 -              ("No such type variable in theorem: " ^
  17.229 -               Syntax.string_of_vname xi);
  17.230 -        val (rtypes, rsorts) = types_sorts thm;
  17.231 -        fun readT (xi, s) =
  17.232 -            let val S = case rsorts xi of SOME S => S | NONE => absent xi;
  17.233 -                val T = ProofContext.read_typ ctxt s;
  17.234 -            in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
  17.235 -               else error
  17.236 -                 ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
  17.237 -            end;
  17.238 -        val Tinsts_env = map readT Tinsts;
  17.239 -        val cenvT = map (apsnd (Thm.ctyp_of sign)) (Tinsts_env);
  17.240 -        val thm' = Thm.instantiate (cenvT, []) thm;
  17.241 -           (* Instantiate, but don't normalise: *)
  17.242 -           (* this happens after term insts anyway. *)
  17.243 +fun instantiate sign envT env =
  17.244 +  let
  17.245 +    fun prepT (a, T) = (a, Thm.ctyp_of sign T);
  17.246 +    fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
  17.247 +  in
  17.248 +    Drule.instantiate (map prepT (distinct envT),
  17.249 +      map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env))
  17.250 +  end;
  17.251 +
  17.252 +in
  17.253 +
  17.254 +fun read_instantiate init mixed_insts (context, thm) =
  17.255 +  let
  17.256 +    val ctxt = init context;
  17.257 +    val sign = ProofContext.sign_of ctxt;
  17.258  
  17.259 -        (* Term instantiations *)
  17.260 -        val vars = Drule.vars_of thm';
  17.261 -        fun get_typ xi =
  17.262 -          (case assoc (vars, xi) of
  17.263 -            SOME T => T
  17.264 -          | NONE => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
  17.265 +    val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
  17.266 +    val internal_insts = term_insts |> List.mapPartial
  17.267 +      (fn (xi, Args.Term t) => SOME (xi, t)
  17.268 +      | (_, Args.Name _) => NONE
  17.269 +      | (xi, _) => error_var "Term argument expected for " xi);
  17.270 +    val external_insts = term_insts |> List.mapPartial
  17.271 +      (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
  17.272  
  17.273 -        val (xs, ss) = Library.split_list tinsts;
  17.274 -        val Ts = map get_typ xs;
  17.275 +
  17.276 +    (* type instantiations *)
  17.277  
  17.278 -        val used = add_term_tvarnames (prop_of thm',[])
  17.279 -        (* Names of TVars occuring in thm'.  read_def_termTs ensures
  17.280 -           that new TVars introduced when reading the instantiation string
  17.281 -           are distinct from those occuring in the theorem. *)
  17.282 -
  17.283 -        val (ts, envT) =
  17.284 -          ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) used (ss ~~ Ts);
  17.285 +    val sorts = #2 (Drule.types_sorts thm);
  17.286  
  17.287 -        val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
  17.288 -        val cenv =
  17.289 -          map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
  17.290 -            (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
  17.291 +    fun readT (xi, arg) =
  17.292 +      let
  17.293 +        val S = the_sort sorts xi;
  17.294 +        val T =
  17.295 +          (case arg of
  17.296 +            Args.Name s => ProofContext.read_typ ctxt s
  17.297 +          | Args.Typ T => T
  17.298 +          | _ => error_var "Type argument expected for " xi);
  17.299        in
  17.300 -        thm'
  17.301 -        |> Drule.instantiate (cenvT, cenv)
  17.302 -        |> RuleCases.save thm
  17.303 +        if Sign.of_sort sign (T, S) then (xi, T)
  17.304 +        else error_var "Incompatible sort for typ instantiation of " xi
  17.305        end;
  17.306  
  17.307 -fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x;
  17.308 +    val type_insts' = map readT type_insts;
  17.309 +    val thm' = instantiate sign type_insts' [] thm;
  17.310 +
  17.311 +
  17.312 +    (* internal term instantiations *)
  17.313 +
  17.314 +    val types' = #1 (Drule.types_sorts thm');
  17.315 +    val unifier = Vartab.dest (#1
  17.316 +      (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts)));
  17.317 +
  17.318 +    val type_insts'' = map (typ_subst unifier) type_insts';
  17.319 +    val internal_insts'' = map (subst unifier) internal_insts;
  17.320 +    val thm'' = instantiate sign unifier internal_insts'' thm';
  17.321 +
  17.322 +
  17.323 +    (* external term instantiations *)
  17.324 +
  17.325 +    val types'' = #1 (Drule.types_sorts thm'');
  17.326 +
  17.327 +    val (xs, ss) = split_list external_insts;
  17.328 +    val Ts = map (the_type types'') xs;
  17.329 +    val (ts, inferred) = ProofContext.read_termTs ctxt (K false)
  17.330 +        (K NONE) (K NONE) (Drule.add_used thm'' []) (ss ~~ Ts);
  17.331 +
  17.332 +    val type_insts''' = map (typ_subst inferred) type_insts'';
  17.333 +    val internal_insts''' = map (subst inferred) internal_insts'';
  17.334  
  17.335 -fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of));
  17.336 +    val external_insts''' = xs ~~ ts;
  17.337 +    val term_insts''' = internal_insts''' @ external_insts''';
  17.338 +    val thm''' = instantiate sign inferred external_insts''' thm'';
  17.339 +  in
  17.340 +
  17.341 +    (* assign internalized values *)
  17.342 +
  17.343 +    mixed_insts |> List.app (fn (arg, (xi, _)) =>
  17.344 +      if is_tvar xi then
  17.345 +        Args.assign (SOME (Args.Typ (valOf (assoc (type_insts''', xi))))) arg
  17.346 +      else
  17.347 +        Args.assign (SOME (Args.Term (valOf (assoc (term_insts''', xi))))) arg);
  17.348 +
  17.349 +    (context, thm''' |> RuleCases.save thm)
  17.350 +  end;
  17.351 +
  17.352 +end;
  17.353 +
  17.354 +
  17.355 +(* where: named instantiation *)
  17.356 +
  17.357 +local
  17.358 +
  17.359 +val value =
  17.360 +  Args.internal_typ >> Args.Typ ||
  17.361 +  Args.internal_term >> Args.Term ||
  17.362 +  Args.name >> Args.Name;
  17.363 +
  17.364 +val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
  17.365 +  >> (fn (xi, (a, v)) => (a, (xi, v)));
  17.366 +
  17.367 +fun gen_where init =
  17.368 +  syntax (Args.and_list (Scan.lift inst) >> read_instantiate init);
  17.369 +
  17.370 +in
  17.371  
  17.372  val where_global = gen_where ProofContext.init;
  17.373  val where_local = gen_where I;
  17.374  
  17.375 +end;
  17.376  
  17.377 -(* of: positional instantiations *)
  17.378 -(*        permits instantiation of term variables only *)
  17.379 +
  17.380 +(* of: positional instantiation (term arguments only) *)
  17.381 +
  17.382 +local
  17.383  
  17.384 -fun read_instantiate' _ ([], []) _ thm = thm
  17.385 -  | read_instantiate' context_of (args, concl_args) x thm =
  17.386 -      let
  17.387 -        fun zip_vars _ [] = []
  17.388 -          | zip_vars (_ :: xs) (NONE :: opt_ts) = zip_vars xs opt_ts
  17.389 -          | zip_vars ((x, _) :: xs) (SOME t :: opt_ts) = (x, t) :: zip_vars xs opt_ts
  17.390 -          | zip_vars [] _ = error "More instantiations than variables in theorem";
  17.391 -        val insts =
  17.392 -          zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
  17.393 -          zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
  17.394 -      in
  17.395 -        thm
  17.396 -        |> read_instantiate context_of insts x
  17.397 -        |> RuleCases.save thm
  17.398 -      end;
  17.399 +fun read_instantiate' init (args, concl_args) (context, thm) =
  17.400 +  let
  17.401 +    fun zip_vars _ [] = []
  17.402 +      | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
  17.403 +      | zip_vars ((x, _) :: xs) ((a, SOME t) :: rest) = (a, (x, t)) :: zip_vars xs rest
  17.404 +      | zip_vars [] _ = error "More instantiations than variables in theorem";
  17.405 +    val insts =
  17.406 +      zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
  17.407 +      zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
  17.408 +  in
  17.409 +    read_instantiate init insts (context, thm)
  17.410 +  end;
  17.411  
  17.412 +val value =
  17.413 +  Args.internal_term >> Args.Term ||
  17.414 +  Args.name >> Args.Name;
  17.415 +
  17.416 +val inst = Args.ahead -- Args.maybe value;
  17.417  val concl = Args.$$$ "concl" -- Args.colon;
  17.418 -val inst_arg = Scan.unless concl Args.name_dummy;
  17.419 -val inst_args = Scan.repeat inst_arg;
  17.420 -fun insts' x = (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;
  17.421  
  17.422 -fun gen_of context_of =
  17.423 -  syntax (Scan.lift insts' >> (Drule.rule_attribute o read_instantiate' context_of));
  17.424 +val insts =
  17.425 +  Scan.repeat (Scan.unless concl inst) --
  17.426 +  Scan.optional (concl |-- Scan.repeat inst) [];
  17.427 +
  17.428 +fun gen_of init = syntax (Scan.lift insts >> read_instantiate' init);
  17.429 +
  17.430 +in
  17.431  
  17.432  val of_global = gen_of ProofContext.init;
  17.433  val of_local = gen_of I;
  17.434  
  17.435 +end;
  17.436 +
  17.437  
  17.438  (* rename_abs *)
  17.439  
  17.440  fun rename_abs src = syntax
  17.441 -  (Scan.lift (Scan.repeat Args.name_dummy >> (apsnd o Drule.rename_bvars'))) src;
  17.442 +  (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'))) src;
  17.443  
  17.444  
  17.445  (* unfold / fold definitions *)
  17.446 @@ -335,9 +434,8 @@
  17.447  
  17.448  (* rule_format *)
  17.449  
  17.450 -fun rule_format_att x = syntax
  17.451 -  (Scan.lift (Args.parens (Args.$$$ "no_asm")
  17.452 -  >> K ObjectLogic.rule_format_no_asm || Scan.succeed ObjectLogic.rule_format)) x;
  17.453 +fun rule_format_att x = syntax (Args.mode "no_asm"
  17.454 +  >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)) x;
  17.455  
  17.456  
  17.457  (* misc rules *)
  17.458 @@ -380,6 +478,20 @@
  17.459  end;
  17.460  
  17.461  
  17.462 +(* internal attribute *)
  17.463 +
  17.464 +val attributeN = "attribute";
  17.465 +fun attribute att = Args.src ((attributeN, [Args.mk_attribute att]), Position.none);
  17.466 +
  17.467 +fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x;
  17.468 +fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x;
  17.469 +
  17.470 +val setup_internal_attribute =
  17.471 + [PureThy.global_path,
  17.472 +  add_attributes [(attributeN, (attribute_global, attribute_local), "internal attribute")],
  17.473 +  PureThy.local_path];
  17.474 +
  17.475 +
  17.476  
  17.477  (** theory setup **)
  17.478  
  17.479 @@ -412,7 +524,8 @@
  17.480  
  17.481  (* setup *)
  17.482  
  17.483 -val setup = [AttributesData.init, add_attributes pure_attributes];
  17.484 +val setup =
  17.485 + AttributesData.init :: setup_internal_attribute @ [add_attributes pure_attributes];
  17.486  
  17.487  end;
  17.488  
    18.1 --- a/src/Pure/Isar/constdefs.ML	Wed Apr 13 09:48:41 2005 +0200
    18.2 +++ b/src/Pure/Isar/constdefs.ML	Wed Apr 13 18:34:22 2005 +0200
    18.3 @@ -11,7 +11,7 @@
    18.4  sig
    18.5    val add_constdefs: (string list * string option) list *
    18.6      ((bstring * string option * Syntax.mixfix) option *
    18.7 -      ((bstring * Args.src list) * string)) list
    18.8 +      ((bstring * Attrib.src list) * string)) list
    18.9      -> theory -> theory
   18.10    val add_constdefs_i: (string list * typ option) list *
   18.11      ((bstring * typ option * Syntax.mixfix) option *
    19.1 --- a/src/Pure/Isar/induct_attrib.ML	Wed Apr 13 09:48:41 2005 +0200
    19.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Apr 13 18:34:22 2005 +0200
    19.3 @@ -204,25 +204,22 @@
    19.4  
    19.5  local
    19.6  
    19.7 -fun spec k cert =
    19.8 -  (Args.$$$ k -- Args.colon) |-- Args.!!! (Args.name >> cert) ||
    19.9 -  Args.$$$ k >> K "";
   19.10 +fun spec k arg =
   19.11 +  Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   19.12 +  Scan.lift (Args.$$$ k) >> K "";
   19.13  
   19.14 -fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   19.15 -  let val sg = sign_of x in
   19.16 -    spec typeN (Sign.certify_tyname sg o Sign.intern_tycon sg) >> add_type ||
   19.17 -    spec setN (Sign.certify_const sg o Sign.intern_const sg) >> add_set
   19.18 -  end >> pair x);
   19.19 +fun attrib tyname const add_type add_set =
   19.20 +  Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
   19.21  
   19.22  in
   19.23  
   19.24  val cases_attr =
   19.25 -  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
   19.26 -   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
   19.27 + (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
   19.28 +  attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
   19.29  
   19.30  val induct_attr =
   19.31 -  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
   19.32 -   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
   19.33 + (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
   19.34 +  attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
   19.35  
   19.36  end;
   19.37  
    20.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 13 09:48:41 2005 +0200
    20.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 13 18:34:22 2005 +0200
    20.3 @@ -47,7 +47,7 @@
    20.4    val print_syntax: Toplevel.transition -> Toplevel.transition
    20.5    val print_theorems: Toplevel.transition -> Toplevel.transition
    20.6    val print_locales: Toplevel.transition -> Toplevel.transition
    20.7 -  val print_locale: Locale.expr * Args.src Locale.element list
    20.8 +  val print_locale: Locale.expr * Locale.element list
    20.9      -> Toplevel.transition -> Toplevel.transition
   20.10    val print_registrations: string -> Toplevel.transition -> Toplevel.transition
   20.11    val print_attributes: Toplevel.transition -> Toplevel.transition
   20.12 @@ -58,14 +58,14 @@
   20.13    val print_antiquotations: Toplevel.transition -> Toplevel.transition
   20.14    val print_thms_containing: int option * string list
   20.15      -> Toplevel.transition -> Toplevel.transition
   20.16 -  val thm_deps: (thmref * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   20.17 +  val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   20.18    val print_binds: Toplevel.transition -> Toplevel.transition
   20.19    val print_lthms: Toplevel.transition -> Toplevel.transition
   20.20    val print_cases: Toplevel.transition -> Toplevel.transition
   20.21    val print_intros: Toplevel.transition -> Toplevel.transition
   20.22 -  val print_thms: string list * (thmref * Args.src list) list
   20.23 +  val print_thms: string list * (thmref * Attrib.src list) list
   20.24      -> Toplevel.transition -> Toplevel.transition
   20.25 -  val print_prfs: bool -> string list * (thmref * Args.src list) list option
   20.26 +  val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
   20.27      -> Toplevel.transition -> Toplevel.transition
   20.28    val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   20.29    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
   20.30 @@ -187,7 +187,7 @@
   20.31  (* present draft files *)
   20.32  
   20.33  fun display_drafts files = Toplevel.imperative (fn () =>
   20.34 -  let val outfile = File.quote_sysify_path (Present.drafts "pdf" files)
   20.35 +  let val outfile = File.quote_sysify_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
   20.36    in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
   20.37  
   20.38  fun print_drafts files = Toplevel.imperative (fn () =>
   20.39 @@ -218,9 +218,7 @@
   20.40    Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
   20.41  
   20.42  fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   20.43 -  let val thy = Toplevel.theory_of state in
   20.44 -    Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body)
   20.45 -  end);
   20.46 +  Locale.print_locale (Toplevel.theory_of state) import body);
   20.47  
   20.48  fun print_registrations name = Toplevel.unknown_context o
   20.49    Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name)
    21.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 13 09:48:41 2005 +0200
    21.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 13 18:34:22 2005 +0200
    21.3 @@ -310,24 +310,22 @@
    21.4          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    21.5        >> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));
    21.6  
    21.7 -val uterm = P.underscore >> K NONE || P.term >> SOME;
    21.8 -
    21.9  val view_val =
   21.10 -  Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") [];
   21.11 +  Scan.optional (P.$$$ "[" |-- Scan.repeat1 (P.maybe P.term) --| P.$$$ "]") [];
   21.12  
   21.13  val interpretationP =
   21.14    OuterSyntax.command "interpretation"
   21.15 -  "prove and register interpretation of locale expression in theory" K.thy_goal
   21.16 -  ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
   21.17 -     >> IsarThy.register_globally)
   21.18 -   >> (Toplevel.print oo Toplevel.theory_to_proof));
   21.19 +    "prove and register interpretation of locale expression in theory" K.thy_goal
   21.20 +    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
   21.21 +      >> ((Toplevel.print oo Toplevel.theory_to_proof) o IsarThy.register_globally));
   21.22  
   21.23  val interpretP =
   21.24    OuterSyntax.command "interpret"
   21.25 -    "prove and register interpretation of locale expression in context"
   21.26 -    K.prf_goal
   21.27 -    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val >>
   21.28 -      ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
   21.29 +    "prove and register interpretation of locale expression in context" K.prf_goal
   21.30 +    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
   21.31 +      >> ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
   21.32 +
   21.33 +
   21.34  
   21.35  (** proof commands **)
   21.36  
   21.37 @@ -427,7 +425,7 @@
   21.38        >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
   21.39  
   21.40  val case_spec =
   21.41 -  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 P.uname --| P.$$$ ")") ||
   21.42 +  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   21.43      P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
   21.44  
   21.45  val caseP =
    22.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Apr 13 09:48:41 2005 +0200
    22.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Apr 13 18:34:22 2005 +0200
    22.3 @@ -9,113 +9,115 @@
    22.4  sig
    22.5    val hide_space: string * xstring list -> theory -> theory
    22.6    val hide_space_i: string * string list -> theory -> theory
    22.7 -  val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    22.8 +  val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    22.9    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
   22.10 -  val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory
   22.11 +  val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
   22.12    val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
   22.13 -  val theorems: string -> ((bstring * Args.src list) * (thmref * Args.src list) list) list
   22.14 +  val theorems: string ->
   22.15 +    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
   22.16      -> theory -> theory * (string * thm list) list
   22.17    val theorems_i: string ->
   22.18      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
   22.19      -> theory -> theory * (string * thm list) list
   22.20    val locale_theorems: string -> xstring ->
   22.21 -    ((bstring * Args.src list) * (thmref * Args.src list) list) list
   22.22 +    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
   22.23      -> theory -> theory * (bstring * thm list) list
   22.24    val locale_theorems_i: string -> string ->
   22.25 -    ((bstring * Locale.multi_attribute list)
   22.26 -      * (thm list * Locale.multi_attribute list) list) list
   22.27 -    -> theory -> theory * (string * thm list) list
   22.28 +    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   22.29 +    theory -> theory * (string * thm list) list
   22.30    val smart_theorems: string -> xstring option ->
   22.31 -    ((bstring * Args.src list) * (thmref * Args.src list) list) list
   22.32 +    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
   22.33      -> theory -> theory * (string * thm list) list
   22.34 -  val declare_theorems: xstring option -> (thmref * Args.src list) list -> theory -> theory
   22.35 -  val apply_theorems: (thmref * Args.src list) list -> theory -> theory * thm list
   22.36 +  val declare_theorems: xstring option ->
   22.37 +    (thmref * Attrib.src list) list -> theory -> theory
   22.38 +  val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list
   22.39    val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
   22.40 -  val have_facts: ((string * Args.src list) * (thmref * Args.src list) list) list
   22.41 +  val have_facts: ((string * Attrib.src list) * (thmref * Attrib.src list) list) list
   22.42      -> ProofHistory.T -> ProofHistory.T
   22.43    val have_facts_i: ((string * Proof.context attribute list) *
   22.44      (thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T
   22.45 -  val from_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   22.46 +  val from_facts: (thmref * Attrib.src list) list list -> ProofHistory.T -> ProofHistory.T
   22.47    val from_facts_i: (thm * Proof.context attribute list) list list
   22.48      -> ProofHistory.T -> ProofHistory.T
   22.49 -  val with_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   22.50 +  val with_facts: (thmref * Attrib.src list) list list -> ProofHistory.T -> ProofHistory.T
   22.51    val with_facts_i: (thm * Proof.context attribute list) list list
   22.52      -> ProofHistory.T -> ProofHistory.T
   22.53 -  val using_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   22.54 +  val using_facts: (thmref * Attrib.src list) list list
   22.55 +    -> ProofHistory.T -> ProofHistory.T
   22.56    val using_facts_i: (thm * Proof.context attribute list) list list
   22.57      -> ProofHistory.T -> ProofHistory.T
   22.58    val chain: ProofHistory.T -> ProofHistory.T
   22.59 -  val instantiate_locale: (string * Args.src list) * string -> ProofHistory.T
   22.60 +  val instantiate_locale: (string * Attrib.src list) * string -> ProofHistory.T
   22.61      -> ProofHistory.T
   22.62    val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
   22.63    val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
   22.64    val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
   22.65    val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
   22.66 -  val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T
   22.67 +  val invoke_case: string * string option list * Attrib.src list -> ProofHistory.T -> ProofHistory.T
   22.68    val invoke_case_i: string * string option list * Proof.context attribute list
   22.69      -> ProofHistory.T -> ProofHistory.T
   22.70 -  val theorem: string -> (bstring * Args.src list) * (string * (string list * string list))
   22.71 +  val theorem: string -> (bstring * Attrib.src list) * (string * (string list * string list))
   22.72      -> bool -> theory -> ProofHistory.T
   22.73    val theorem_i: string -> (bstring * theory attribute list) *
   22.74      (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
   22.75 -  val multi_theorem:
   22.76 -    string -> (theory -> theory) -> 
   22.77 +  val multi_theorem: string -> (theory -> theory) ->
   22.78      (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
   22.79 -    bstring * Args.src list
   22.80 -    -> Args.src Locale.element Locale.elem_expr list
   22.81 -    -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
   22.82 +    bstring * Attrib.src list -> Locale.element Locale.elem_expr list ->
   22.83 +    ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
   22.84      -> bool -> theory -> ProofHistory.T
   22.85 -  val multi_theorem_i:
   22.86 -    string -> (theory -> theory) ->  
   22.87 +  val multi_theorem_i: string -> (theory -> theory) ->
   22.88      (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
   22.89 -    bstring * theory attribute list
   22.90 -    -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
   22.91 +    bstring * theory attribute list -> Locale.element_i Locale.elem_expr list
   22.92      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
   22.93      -> bool -> theory -> ProofHistory.T
   22.94    val locale_multi_theorem: string -> xstring
   22.95 -    -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
   22.96 -    -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
   22.97 +    -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
   22.98 +    -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
   22.99      -> bool -> theory -> ProofHistory.T
  22.100 -  val locale_multi_theorem_i: string -> string -> bstring * Locale.multi_attribute list
  22.101 -    -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
  22.102 -    -> ((bstring * Locale.multi_attribute list) * (term * (term list * term list)) list) list
  22.103 +  val locale_multi_theorem_i: string -> string -> bstring * Attrib.src list
  22.104 +    -> Locale.element_i Locale.elem_expr list
  22.105 +    -> ((bstring * Attrib.src list) * (term * (term list * term list)) list) list
  22.106      -> bool -> theory -> ProofHistory.T
  22.107    val smart_multi_theorem: string -> xstring option
  22.108 -    -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
  22.109 -    -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
  22.110 +    -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
  22.111 +    -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
  22.112      -> bool -> theory -> ProofHistory.T
  22.113 -  val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
  22.114 +  val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
  22.115      -> ProofHistory.T -> ProofHistory.T
  22.116    val assume_i:
  22.117      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
  22.118      -> ProofHistory.T -> ProofHistory.T
  22.119 -  val presume: ((string * Args.src list) * (string * (string list * string list)) list) list
  22.120 +  val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
  22.121      -> ProofHistory.T -> ProofHistory.T
  22.122    val presume_i:
  22.123      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
  22.124      -> ProofHistory.T -> ProofHistory.T
  22.125 -  val have: ((string * Args.src list) * (string * (string list * string list)) list) list
  22.126 -    -> ProofHistory.T -> ProofHistory.T
  22.127 +  val have: ((string * Attrib.src list) *
  22.128 +    (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T
  22.129    val have_i: ((string * Proof.context attribute list) *
  22.130      (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
  22.131 -  val hence: ((string * Args.src list) * (string * (string list * string list)) list) list
  22.132 -    -> ProofHistory.T -> ProofHistory.T
  22.133 +  val hence: ((string * Attrib.src list) *
  22.134 +    (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T
  22.135    val hence_i: ((string * Proof.context attribute list) *
  22.136      (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
  22.137 -  val show: ((string * Args.src list) * (string * (string list * string list)) list) list
  22.138 +  val show: ((string * Attrib.src list) *
  22.139 +    (string * (string list * string list)) list) list
  22.140      -> bool -> ProofHistory.T -> ProofHistory.T
  22.141    val show_i: ((string * Proof.context attribute list) *
  22.142 -    (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
  22.143 -  val thus: ((string * Args.src list) * (string * (string list * string list)) list) list
  22.144 +    (term * (term list * term list)) list) list
  22.145 +    -> bool -> ProofHistory.T -> ProofHistory.T
  22.146 +  val thus: ((string * Attrib.src list) *
  22.147 +    (string * (string list * string list)) list) list
  22.148      -> bool -> ProofHistory.T -> ProofHistory.T
  22.149    val thus_i: ((string * Proof.context attribute list)
  22.150 -    * (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
  22.151 -  val local_def: (string * Args.src list) * (string * (string * string list))
  22.152 +    * (term * (term list * term list)) list) list
  22.153 +    -> bool -> ProofHistory.T -> ProofHistory.T
  22.154 +  val local_def: (string * Attrib.src list) * (string * (string * string list))
  22.155      -> ProofHistory.T -> ProofHistory.T
  22.156 -  val local_def_i: (string * Args.src list) * (string * (term * term list))
  22.157 +  val local_def_i: (string * Attrib.src list) * (string * (term * term list))
  22.158      -> ProofHistory.T -> ProofHistory.T
  22.159    val obtain: (string list * string option) list
  22.160 -    * ((string * Args.src list) * (string * (string list * string list)) list) list
  22.161 +    * ((string * Attrib.src list) * (string * (string list * string list)) list) list
  22.162      -> Toplevel.transition -> Toplevel.transition
  22.163    val obtain_i: (string list * typ option) list
  22.164      * ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
  22.165 @@ -136,10 +138,10 @@
  22.166    val done_proof: Toplevel.transition -> Toplevel.transition
  22.167    val skip_proof: Toplevel.transition -> Toplevel.transition
  22.168    val forget_proof: Toplevel.transition -> Toplevel.transition
  22.169 -  val get_thmss: (thmref * Args.src list) list -> Proof.state -> thm list
  22.170 -  val also: (thmref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
  22.171 +  val get_thmss: (thmref * Attrib.src list) list -> Proof.state -> thm list
  22.172 +  val also: (thmref * Attrib.src list) list option -> Toplevel.transition -> Toplevel.transition
  22.173    val also_i: thm list option -> Toplevel.transition -> Toplevel.transition
  22.174 -  val finally: (thmref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
  22.175 +  val finally: (thmref * Attrib.src list) list option -> Toplevel.transition -> Toplevel.transition
  22.176    val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition
  22.177    val moreover: Toplevel.transition -> Toplevel.transition
  22.178    val ultimately: Toplevel.transition -> Toplevel.transition
  22.179 @@ -151,7 +153,13 @@
  22.180    val token_translation: string -> theory -> theory
  22.181    val method_setup: bstring * string * string -> theory -> theory
  22.182    val add_oracle: bstring * string -> theory -> theory
  22.183 -  val add_locale: bool * bstring * Locale.expr * Args.src Locale.element list -> theory -> theory
  22.184 +  val add_locale: bool * bstring * Locale.expr * Locale.element list -> theory -> theory
  22.185 +  val register_globally:
  22.186 +    ((string * Attrib.src list) * Locale.expr) * string option list ->
  22.187 +    bool -> theory -> ProofHistory.T
  22.188 +  val register_locally:
  22.189 +    ((string * Attrib.src list) * Locale.expr) * string option list ->
  22.190 +    ProofHistory.T -> ProofHistory.T
  22.191    val begin_theory: string -> string list -> (string * bool) list -> theory
  22.192    val end_theory: theory -> theory
  22.193    val kill_theory: string -> unit
  22.194 @@ -159,14 +167,6 @@
  22.195      -> Toplevel.transition -> Toplevel.transition
  22.196    val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
  22.197    val context: string -> Toplevel.transition -> Toplevel.transition
  22.198 -
  22.199 -  val register_globally:
  22.200 -    ((string * Args.src list) * Locale.expr) * string option list ->
  22.201 -    bool -> theory -> ProofHistory.T
  22.202 -  val register_locally:
  22.203 -    ((string * Args.src list) * Locale.expr) * string option list ->
  22.204 -    ProofHistory.T -> ProofHistory.T
  22.205 -
  22.206  end;
  22.207  
  22.208  structure IsarThy: ISAR_THY =
  22.209 @@ -180,8 +180,8 @@
  22.210  
  22.211  val kinds =
  22.212   [(Sign.classK, can o Sign.certify_class),
  22.213 -  (Sign.typeK, can o Sign.certify_tyname),
  22.214 -  (Sign.constK, can o Sign.certify_const)];
  22.215 +  (Sign.typeK, Sign.declared_tyname),
  22.216 +  (Sign.constK, Sign.declared_const)];
  22.217  
  22.218  fun gen_hide intern (kind, xnames) thy =
  22.219    (case assoc (kinds, kind) of
  22.220 @@ -226,7 +226,6 @@
  22.221  
  22.222  fun global_attribs thy = prep_attribs (Attrib.global_attribute thy);
  22.223  fun local_attribs thy = prep_attribs (Attrib.local_attribute thy);
  22.224 -fun multi_attribs thy = prep_attribs (Attrib.multi_attribute thy);
  22.225  
  22.226  end;
  22.227  
  22.228 @@ -250,13 +249,13 @@
  22.229    |> present_thmss k;
  22.230  
  22.231  fun locale_theorems k loc args thy = thy
  22.232 -  |> Locale.note_thmss k loc (multi_attribs thy args)
  22.233 +  |> Locale.note_thmss k loc args
  22.234    |> present_thmss k;
  22.235  
  22.236  fun smart_theorems k opt_loc args thy = thy
  22.237    |> (case opt_loc of
  22.238      NONE => PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
  22.239 -  | SOME loc => Locale.note_thmss k loc (multi_attribs thy args))
  22.240 +  | SOME loc => Locale.note_thmss k loc args)
  22.241    |> present_thmss k;
  22.242  
  22.243  fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
  22.244 @@ -384,28 +383,33 @@
  22.245  
  22.246  in
  22.247  
  22.248 -fun multi_theorem k thy_mod export a elems concl int thy =
  22.249 -  global_statement (Proof.multi_theorem k thy_mod export NONE (apsnd (map (Attrib.global_attribute thy)) a)
  22.250 -    (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems)) concl int thy;
  22.251 +fun multi_theorem k after_qed export a elems concl int thy =
  22.252 +  global_statement (Proof.multi_theorem k after_qed export NONE
  22.253 +    (apsnd (map (Attrib.global_attribute thy)) a)
  22.254 +    (map (Locale.intern_attrib_elem_expr thy) elems)) concl int thy;
  22.255  
  22.256 -fun multi_theorem_i k thy_mod export a = global_statement_i o Proof.multi_theorem_i k thy_mod export NONE a;
  22.257 +fun multi_theorem_i k after_qed export a =
  22.258 +  global_statement_i o Proof.multi_theorem_i k after_qed export NONE a;
  22.259  
  22.260  fun locale_multi_theorem k locale (name, atts) elems concl int thy =
  22.261 -  global_statement (Proof.multi_theorem k I ProofContext.export_standard
  22.262 -      (SOME (locale, (map (Attrib.multi_attribute thy) atts,
  22.263 -          map (map (Attrib.multi_attribute thy) o snd o fst) concl)))
  22.264 -      (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems))
  22.265 -      (map (apfst (apsnd (K []))) concl) int thy;
  22.266 +  global_statement (Proof.multi_theorem k I  ProofContext.export_standard
  22.267 +      (SOME (locale,
  22.268 +        (map (Attrib.intern_src (Theory.sign_of thy)) atts,
  22.269 +         map (map (Attrib.intern_src (Theory.sign_of thy)) o snd o fst) concl)))
  22.270 +      (name, [])
  22.271 +      (map (Locale.intern_attrib_elem_expr thy) elems))
  22.272 +    (map (apfst (apsnd (K []))) concl) int thy;
  22.273  
  22.274  fun locale_multi_theorem_i k locale (name, atts) elems concl =
  22.275    global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard
  22.276        (SOME (locale, (atts, map (snd o fst) concl)))
  22.277        (name, []) elems) (map (apfst (apsnd (K []))) concl);
  22.278  
  22.279 -fun theorem k (a, t) = multi_theorem k I ProofContext.export_standard
  22.280 -       a [] [(("", []), [t])];
  22.281 -fun theorem_i k (a, t) = multi_theorem_i k I ProofContext.export_standard
  22.282 -       a [] [(("", []), [t])];
  22.283 +fun theorem k (a, t) =
  22.284 +  multi_theorem k I ProofContext.export_standard a [] [(("", []), [t])];
  22.285 +
  22.286 +fun theorem_i k (a, t) =
  22.287 +  multi_theorem_i k I ProofContext.export_standard a [] [(("", []), [t])];
  22.288  
  22.289  fun smart_multi_theorem k NONE a elems =
  22.290        multi_theorem k I ProofContext.export_standard a elems
  22.291 @@ -583,7 +587,7 @@
  22.292    Context.use_let
  22.293      "val thm = PureThy.get_thm_closure (Context.the_context ());\n\
  22.294      \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
  22.295 -    \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string"
  22.296 +    \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
  22.297      "PureIsar.Method.add_method method"
  22.298      ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
  22.299  
  22.300 @@ -600,8 +604,43 @@
  22.301  (* add_locale *)
  22.302  
  22.303  fun add_locale (do_pred, name, import, body) thy =
  22.304 -  Locale.add_locale do_pred name import
  22.305 -    (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body) thy;
  22.306 +  Locale.add_locale do_pred name import body thy;
  22.307 +
  22.308 +
  22.309 +(* registration of locale interpretations *)
  22.310 +
  22.311 +fun register_globally (((prfx, atts), expr), insts) int thy =
  22.312 +  let
  22.313 +    val (thy', propss, activate) =
  22.314 +      Locale.prep_global_registration (prfx, atts) expr insts thy;
  22.315 +    fun witness id (thy, thm) = let
  22.316 +        val thm' = Drule.freeze_all thm;
  22.317 +      in
  22.318 +        (Locale.add_global_witness id thm' thy, thm')
  22.319 +      end;
  22.320 +  in
  22.321 +    multi_theorem_i Drule.internalK activate ProofContext.export_plain
  22.322 +      ("", []) []
  22.323 +      (map (fn ((n, ps), props) => 
  22.324 +          ((NameSpace.base n, [witness (n, map Logic.varify ps)]), 
  22.325 +        map (fn prop => (prop, ([], []))) props)) propss) int thy'
  22.326 +  end;
  22.327 +
  22.328 +fun register_locally (((prfx, atts), expr), insts) =
  22.329 +  ProofHistory.apply (fn state =>
  22.330 +    let
  22.331 +      val ctxt = Proof.context_of state;
  22.332 +      val (ctxt', propss, activate) =
  22.333 +        Locale.prep_local_registration (prfx, atts) expr insts ctxt;
  22.334 +      fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
  22.335 +    in
  22.336 +      state
  22.337 +      |> Proof.map_context (fn _ => ctxt')
  22.338 +      |> Proof.have_i (Seq.single o Proof.map_context activate) true
  22.339 +        (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
  22.340 +          map (fn prop => (prop, ([], []))) props)) propss)
  22.341 +    end);
  22.342 +
  22.343  
  22.344  (* theory init and exit *)
  22.345  
  22.346 @@ -638,38 +677,4 @@
  22.347  
  22.348  val context = init_context (ThyInfo.quiet_update_thy true);
  22.349  
  22.350 -
  22.351 -(* registration of locale interpretation *)
  22.352 -
  22.353 -fun register_globally (((prfx, atts), expr), insts) b thy =
  22.354 -  let
  22.355 -    val (thy', propss, activate) = Locale.prep_global_registration
  22.356 -          (prfx, map (Attrib.global_attribute thy) atts) expr insts thy;
  22.357 -    fun witness id (thy, thm) = let
  22.358 -        val thm' = Drule.freeze_all thm;
  22.359 -      in
  22.360 -        (Locale.add_global_witness id thm' thy, thm')
  22.361 -      end;
  22.362 -  in
  22.363 -    multi_theorem_i Drule.internalK activate ProofContext.export_plain
  22.364 -      ("", []) [] 
  22.365 -      (map (fn ((n, ps), props) => 
  22.366 -          ((NameSpace.base n, [witness (n, map Logic.varify ps)]), 
  22.367 -        map (fn prop => (prop, ([], []))) props)) propss) b thy'
  22.368 -  end;
  22.369 -
  22.370 -fun register_locally (((prfx, atts), expr), insts) =
  22.371 -  ProofHistory.apply (fn state =>
  22.372 -    let
  22.373 -      val ctxt = Proof.context_of state;
  22.374 -      val (ctxt', propss, activate) = Locale.prep_local_registration
  22.375 -            (prfx, map (Attrib.local_attribute' ctxt) atts) expr insts ctxt;
  22.376 -      fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
  22.377 -    in state
  22.378 -      |> Proof.map_context (fn _ => ctxt')
  22.379 -      |> Proof.interpret_i activate Seq.single true
  22.380 -           (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
  22.381 -             map (fn prop => (prop, ([], []))) props)) propss)
  22.382 -    end);
  22.383 -
  22.384  end;
    23.1 --- a/src/Pure/Isar/locale.ML	Wed Apr 13 09:48:41 2005 +0200
    23.2 +++ b/src/Pure/Isar/locale.ML	Wed Apr 13 18:34:22 2005 +0200
    23.3 @@ -21,15 +21,11 @@
    23.4  signature LOCALE =
    23.5  sig
    23.6    type context
    23.7 -  type multi_attribute
    23.8 -
    23.9 -  (* Constructors for elem, expr and elem_expr are
   23.10 -     currently only used for inputting locales (outer_parse.ML). *)
   23.11 -  datatype ('typ, 'term, 'fact, 'att) elem =
   23.12 +  datatype ('typ, 'term, 'fact) elem =
   23.13      Fixes of (string * 'typ option * mixfix option) list |
   23.14 -    Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
   23.15 -    Defines of ((string * 'att list) * ('term * 'term list)) list |
   23.16 -    Notes of ((string * 'att list) * ('fact * 'att list) list) list
   23.17 +    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
   23.18 +    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
   23.19 +    Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
   23.20    datatype expr =
   23.21      Locale of string |
   23.22      Rename of expr * string option list |
   23.23 @@ -38,69 +34,57 @@
   23.24    datatype 'a elem_expr = Elem of 'a | Expr of expr
   23.25  
   23.26    (* Abstract interface to locales *)
   23.27 -  type 'att element
   23.28 -  type 'att element_i
   23.29 +  type element
   23.30 +  type element_i
   23.31    type locale
   23.32    val intern: Sign.sg -> xstring -> string
   23.33    val cond_extern: Sign.sg -> string -> xstring
   23.34    val the_locale: theory -> string -> locale
   23.35 -  val map_attrib_element: ('att -> multi_attribute) -> 'att element ->
   23.36 -    multi_attribute element
   23.37 -  val map_attrib_element_i: ('att -> multi_attribute) -> 'att element_i ->
   23.38 -    multi_attribute element_i
   23.39 -  val map_attrib_elem_or_expr: ('att -> multi_attribute) ->
   23.40 -    'att element elem_expr -> multi_attribute element elem_expr
   23.41 -  val map_attrib_elem_or_expr_i: ('att -> multi_attribute) ->
   23.42 -    'att element_i elem_expr -> multi_attribute element_i elem_expr
   23.43 +  val intern_attrib_elem: theory ->
   23.44 +    ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
   23.45 +  val intern_attrib_elem_expr: theory ->
   23.46 +    ('typ, 'term, 'fact) elem elem_expr -> ('typ, 'term, 'fact) elem elem_expr
   23.47  
   23.48    (* Processing of locale statements *)
   23.49 -  val read_context_statement: xstring option ->
   23.50 -    multi_attribute element elem_expr list ->
   23.51 +  val read_context_statement: xstring option -> element elem_expr list ->
   23.52      (string * (string list * string list)) list list -> context ->
   23.53      string option * (cterm list * cterm list) * context * context * 
   23.54        (term * (term list * term list)) list list
   23.55 -  val cert_context_statement: string option ->
   23.56 -    multi_attribute element_i elem_expr list ->
   23.57 +  val cert_context_statement: string option -> element_i elem_expr list ->
   23.58      (term * (term list * term list)) list list -> context ->
   23.59      string option * (cterm list * cterm list) * context * context *
   23.60        (term * (term list * term list)) list list
   23.61  
   23.62    (* Diagnostic functions *)
   23.63    val print_locales: theory -> unit
   23.64 -  val print_locale: theory -> expr -> multi_attribute element list -> unit
   23.65 +  val print_locale: theory -> expr -> element list -> unit
   23.66    val print_global_registrations: string -> theory -> unit
   23.67 +  val print_local_registrations': string -> context -> unit
   23.68    val print_local_registrations: string -> context -> unit
   23.69  
   23.70    (* Storing results *)
   23.71 -  val add_locale:
   23.72 -    bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
   23.73 -  val add_locale_i:
   23.74 -    bool -> bstring -> expr -> multi_attribute element_i list ->
   23.75 -    theory -> theory
   23.76 -  val smart_note_thmss:
   23.77 -    string -> (string * 'a) option ->
   23.78 +  val add_locale: bool -> bstring -> expr -> element list -> theory -> theory
   23.79 +  val add_locale_i: bool -> bstring -> expr -> element_i list -> theory -> theory
   23.80 +  val smart_note_thmss: string -> string option ->
   23.81      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
   23.82      theory -> theory * (bstring * thm list) list
   23.83 -  val note_thmss:
   23.84 -    string -> xstring ->
   23.85 -    ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->
   23.86 +  val note_thmss: string -> xstring ->
   23.87 +    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
   23.88      theory -> theory * (bstring * thm list) list
   23.89 -  val note_thmss_i:
   23.90 -    string -> string ->
   23.91 -    ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->
   23.92 +  val note_thmss_i: string -> string ->
   23.93 +    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   23.94      theory -> theory * (bstring * thm list) list
   23.95 -  val add_thmss:
   23.96 -    string -> string -> ((string * thm list) * multi_attribute list) list ->
   23.97 +  val add_thmss: string -> string -> ((string * thm list) * Attrib.src list) list ->
   23.98      theory * context -> (theory * context) * (string * thm list) list
   23.99  
  23.100    (* Locale interpretation *)
  23.101    val instantiate: string -> string * context attribute list
  23.102      -> thm list option -> context -> context
  23.103    val prep_global_registration:
  23.104 -    string * theory attribute list -> expr -> string option list -> theory ->
  23.105 +    string * Attrib.src list -> expr -> string option list -> theory ->
  23.106      theory * ((string * term list) * term list) list * (theory -> theory)
  23.107    val prep_local_registration:
  23.108 -    string * context attribute list -> expr -> string option list -> context ->
  23.109 +    string * Attrib.src list -> expr -> string option list -> context ->
  23.110      context * ((string * term list) * term list) list * (context -> context)
  23.111    val add_global_witness:
  23.112      string * term list -> thm -> theory -> theory
  23.113 @@ -118,15 +102,11 @@
  23.114  
  23.115  type context = ProofContext.context;
  23.116  
  23.117 -(* Locales store theory attributes (for activation in theories)
  23.118 -   and context attributes (for activation in contexts) *)
  23.119 -type multi_attribute = theory attribute * context attribute;
  23.120 -
  23.121 -datatype ('typ, 'term, 'fact, 'att) elem =
  23.122 +datatype ('typ, 'term, 'fact) elem =
  23.123    Fixes of (string * 'typ option * mixfix option) list |
  23.124 -  Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
  23.125 -  Defines of ((string * 'att list) * ('term * 'term list)) list |
  23.126 -  Notes of ((string * 'att list) * ('fact * 'att list) list) list;
  23.127 +  Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
  23.128 +  Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
  23.129 +  Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
  23.130  
  23.131  datatype expr =
  23.132    Locale of string |
  23.133 @@ -138,8 +118,8 @@
  23.134  datatype 'a elem_expr =
  23.135    Elem of 'a | Expr of expr;
  23.136  
  23.137 -type 'att element = (string, string, thmref, 'att) elem;
  23.138 -type 'att element_i = (typ, term, thm list, 'att) elem;
  23.139 +type element = (string, string, thmref) elem;
  23.140 +type element_i = (typ, term, thm list) elem;
  23.141  
  23.142  type locale =
  23.143   {predicate: cterm list * thm list,
  23.144 @@ -153,10 +133,17 @@
  23.145         (cf. [1], normalisation of locale expressions.)
  23.146      *)
  23.147    import: expr,                                       (*dynamic import*)
  23.148 -  elems: (multi_attribute element_i * stamp) list,    (*static content*)
  23.149 +  elems: (element_i * stamp) list,                    (*static content*)
  23.150    params: (string * typ option) list * string list}   (*all/local params*)
  23.151  
  23.152  
  23.153 +(* CB: an internal (Int) locale element was either imported or included,
  23.154 +   an external (Ext) element appears directly in the locale text. *)
  23.155 +
  23.156 +datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
  23.157 +
  23.158 +
  23.159 +
  23.160  (** theory data **)
  23.161  
  23.162  structure Termlisttab = TableFun(type key = term list
  23.163 @@ -166,7 +153,7 @@
  23.164  struct
  23.165    val name = "Isar/locales";
  23.166    type T = NameSpace.T * locale Symtab.table *
  23.167 -      ((string * theory attribute list) * thm list) Termlisttab.table
  23.168 +      ((string * Attrib.src list) * thm list) Termlisttab.table
  23.169          Symtab.table;
  23.170      (* 1st entry: locale namespace,
  23.171         2nd entry: locales of the theory,
  23.172 @@ -202,7 +189,7 @@
  23.173  structure LocalLocalesArgs =
  23.174  struct
  23.175    val name = "Isar/locales";
  23.176 -  type T = ((string * context attribute list) * thm list) Termlisttab.table
  23.177 +  type T = ((string * Args.src list) * thm list) Termlisttab.table
  23.178             Symtab.table;
  23.179      (* registrations: theorems instantiating locale assumptions,
  23.180           with prefix and attributes, indexed by locale name and parameter
  23.181 @@ -343,21 +330,23 @@
  23.182  
  23.183  (* printing of registrations *)
  23.184  
  23.185 -fun gen_print_registrations get_regs get_sign msg loc thy_ctxt =
  23.186 +fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt =
  23.187    let
  23.188 -    val sg = get_sign thy_ctxt;
  23.189 +    val ctxt = mk_ctxt thy_ctxt;
  23.190 +    val thy = ProofContext.theory_of ctxt;
  23.191 +    val sg = Theory.sign_of thy;
  23.192 +
  23.193 +    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
  23.194 +    val prt_atts = Args.pretty_attribs ctxt;
  23.195 +    fun prt_inst (ts, (("", []), thms)) =
  23.196 +          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))
  23.197 +      | prt_inst (ts, ((prfx, atts), thms)) =
  23.198 +          Pretty.block (Pretty.breaks
  23.199 +            (Pretty.str prfx :: prt_atts atts @ [Pretty.str ":", Pretty.brk 1,
  23.200 +              Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))]));
  23.201 +
  23.202      val loc_int = intern sg loc;
  23.203      val regs = get_regs thy_ctxt;
  23.204 -    val prt_term = Pretty.quote o Sign.pretty_term sg;
  23.205 -    fun prt_inst (ts, ((prfx, _), thms)) =
  23.206 -         let
  23.207 -           val pp_ts = Pretty.enclose "(" ")"
  23.208 -             (Pretty.breaks (map prt_term ts));
  23.209 -         in
  23.210 -           if prfx = "" then Pretty.block [pp_ts]
  23.211 -           else Pretty.block
  23.212 -             [Pretty.str prfx, Pretty.str ":", Pretty.brk 1, pp_ts]
  23.213 -         end;
  23.214      val loc_regs = Symtab.lookup (regs, loc_int);
  23.215    in
  23.216      (case loc_regs of
  23.217 @@ -369,10 +358,10 @@
  23.218  
  23.219  val print_global_registrations =
  23.220       gen_print_registrations (#3 o GlobalLocalesData.get)
  23.221 -       Theory.sign_of "theory";
  23.222 +       ProofContext.init "theory";
  23.223  val print_local_registrations' =
  23.224       gen_print_registrations LocalLocalesData.get
  23.225 -       ProofContext.sign_of "context";
  23.226 +       I "context";
  23.227  fun print_local_registrations loc ctxt =
  23.228    (print_global_registrations loc (ProofContext.theory_of ctxt);
  23.229     print_local_registrations' loc ctxt);
  23.230 @@ -399,10 +388,47 @@
  23.231  
  23.232  (** primitives **)
  23.233  
  23.234 +(* map elements *)
  23.235 +
  23.236 +fun map_elem {name, var, typ, term, fact, attrib} =
  23.237 +  fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
  23.238 +       let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
  23.239 +   | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
  23.240 +      ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
  23.241 +        (term t, (map term ps, map term qs))))))
  23.242 +   | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
  23.243 +      ((name a, map attrib atts), (term t, map term ps))))
  23.244 +   | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
  23.245 +      ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
  23.246 +
  23.247 +fun map_values typ term thm = map_elem
  23.248 +  {name = I, var = I, typ = typ, term = term, fact = map thm,
  23.249 +    attrib = Args.map_values I typ term thm};
  23.250 +
  23.251 +
  23.252 +(* map attributes *)
  23.253 +
  23.254 +fun map_attrib_specs f = map (apfst (apsnd (map f)));
  23.255 +fun map_attrib_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
  23.256 +
  23.257 +fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f};
  23.258 +
  23.259 +fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy));
  23.260 +
  23.261 +fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem)
  23.262 +  | intern_attrib_elem_expr _ (Expr expr) = Expr expr;
  23.263 +
  23.264 +
  23.265  (* renaming *)
  23.266  
  23.267  fun rename ren x = getOpt (assoc_string (ren, x), x);
  23.268  
  23.269 +fun rename_var ren (x, mx) =
  23.270 +  let val x' = rename ren x in
  23.271 +    if x = x' then (x, mx)
  23.272 +    else (x', if mx = NONE then mx else SOME Syntax.NoSyn)    (*drop syntax*)
  23.273 +  end;
  23.274 +
  23.275  fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
  23.276    | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
  23.277    | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
  23.278 @@ -427,16 +453,9 @@
  23.279        |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps))
  23.280    end;
  23.281  
  23.282 -fun rename_elem ren (Fixes fixes) = Fixes (fixes |> map (fn (x, T, mx) =>
  23.283 -      let val x' = rename ren x in
  23.284 -        if x = x' then (x, T, mx)
  23.285 -        else (x', T, if mx = NONE then mx else SOME Syntax.NoSyn)    (*drop syntax*)
  23.286 -      end))
  23.287 -  | rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
  23.288 -      (rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms)
  23.289 -  | rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
  23.290 -      (rename_term ren t, map (rename_term ren) ps))) defs)
  23.291 -  | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts);
  23.292 +fun rename_elem ren =
  23.293 +  map_values I (rename_term ren) (rename_thm ren) o
  23.294 +  map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
  23.295  
  23.296  fun rename_facts prfx elem =
  23.297    let
  23.298 @@ -481,14 +500,8 @@
  23.299                (map (Thm.assume o cert o inst_term env') hyps))
  23.300        end;
  23.301  
  23.302 -fun inst_elem _ env (Fixes fixes) =
  23.303 -      Fixes (map (fn (x, T, mx) => (x, Option.map (inst_type env) T, mx)) fixes)
  23.304 -  | inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
  23.305 -      (inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms)
  23.306 -  | inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
  23.307 -      (inst_term env t, map (inst_term env) ps))) defs)
  23.308 -  | inst_elem ctxt env (Notes facts) =
  23.309 -      Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);
  23.310 +fun inst_elem ctxt env =
  23.311 +  map_values (inst_type env) (inst_term env) (inst_thm ctxt env);
  23.312  
  23.313  
  23.314  (* term and type instantiation, variant using symbol tables *)
  23.315 @@ -843,36 +856,6 @@
  23.316  end;
  23.317  
  23.318  
  23.319 -(* attributes *)
  23.320 -
  23.321 -local
  23.322 -
  23.323 -fun read_att attrib (x, srcs) = (x, map attrib srcs)
  23.324 -
  23.325 -(* CB: Map attrib over
  23.326 -   * A context element: add attrib to attribute lists of assumptions,
  23.327 -     definitions and facts (on both sides for facts).
  23.328 -   * Locale expression: no effect. *)
  23.329 -
  23.330 -fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes
  23.331 -  | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
  23.332 -  | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
  23.333 -  | gen_map_attrib_elem attrib (Notes facts) =
  23.334 -      Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
  23.335 -
  23.336 -fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)
  23.337 -  | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;
  23.338 -
  23.339 -in
  23.340 -
  23.341 -val map_attrib_element = gen_map_attrib_elem;
  23.342 -val map_attrib_element_i = gen_map_attrib_elem;
  23.343 -val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;
  23.344 -val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;
  23.345 -
  23.346 -end;
  23.347 -
  23.348 -
  23.349  (* activate elements *)
  23.350  
  23.351  local
  23.352 @@ -888,29 +871,26 @@
  23.353        ((ctxt |> ProofContext.add_fixes fixes, axs), [])
  23.354    | activate_elem _ ((ctxt, axs), Assumes asms) =
  23.355        let
  23.356 -        (* extract context attributes *)
  23.357 -        val (Assumes asms) = map_attrib_element_i snd (Assumes asms);
  23.358 -        val ts = List.concat (map (map #1 o #2) asms);
  23.359 -        val (ps,qs) = splitAt (length ts, axs);
  23.360 +        val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms;
  23.361 +        val ts = List.concat (map (map #1 o #2) asms');
  23.362 +        val (ps, qs) = splitAt (length ts, axs);
  23.363          val (ctxt', _) =
  23.364            ctxt |> ProofContext.fix_frees ts
  23.365 -          |> ProofContext.assume_i (export_axioms ps) asms;
  23.366 +          |> ProofContext.assume_i (export_axioms ps) asms';
  23.367        in ((ctxt', qs), []) end
  23.368    | activate_elem _ ((ctxt, axs), Defines defs) =
  23.369        let
  23.370 -        (* extract context attributes *)
  23.371 -        val (Defines defs) = map_attrib_element_i snd (Defines defs);
  23.372 +        val defs' = map_attrib_specs (Attrib.context_attribute_i ctxt) defs;
  23.373          val (ctxt', _) =
  23.374          ctxt |> ProofContext.assume_i ProofContext.export_def
  23.375 -          (defs |> map (fn ((name, atts), (t, ps)) =>
  23.376 +          (defs' |> map (fn ((name, atts), (t, ps)) =>
  23.377              let val (c, t') = ProofContext.cert_def ctxt t
  23.378              in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
  23.379        in ((ctxt', axs), []) end
  23.380    | activate_elem is_ext ((ctxt, axs), Notes facts) =
  23.381        let
  23.382 -        (* extract context attributes *)
  23.383 -        val (Notes facts) = map_attrib_element_i snd (Notes facts);
  23.384 -        val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
  23.385 +        val facts' = map_attrib_facts (Attrib.context_attribute_i ctxt) facts;
  23.386 +        val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts';
  23.387        in ((ctxt', axs), if is_ext then res else []) end;
  23.388  
  23.389  fun activate_elems (((name, ps), axs), elems) ctxt =
  23.390 @@ -930,7 +910,8 @@
  23.391    let
  23.392      val elems = map (prep_facts ctxt) raw_elems;
  23.393      val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt);
  23.394 -  in (ctxt', (((name, ps), elems), res)) end);
  23.395 +    val elems' = map (map_attrib_elem Args.closure) elems;
  23.396 +  in (ctxt', (((name, ps), elems'), res)) end);
  23.397  
  23.398  in
  23.399  
  23.400 @@ -942,12 +923,18 @@
  23.401     assumptions use the axioms in the identifiers to set up exporters
  23.402     in ctxt'.  elemss' does not contain identifiers and is obtained
  23.403     from elemss and the intermediate context with prep_facts.
  23.404 -   If get_facts or get_facts_i is used for prep_facts, these also remove
  23.405 +   If read_facts or cert_facts is used for prep_facts, these also remove
  23.406     the internal/external markers from elemss. *)
  23.407  
  23.408  fun activate_facts prep_facts arg =
  23.409    apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg);
  23.410  
  23.411 +fun activate_note prep_facts (ctxt, args) =
  23.412 +  let
  23.413 +    val (ctxt', ([(_, [Notes args'])], facts)) =
  23.414 +      activate_facts prep_facts (ctxt, [((("", []), []), [Ext (Notes args)])]);
  23.415 +  in (ctxt', (args', facts)) end;
  23.416 +
  23.417  end;
  23.418  
  23.419  
  23.420 @@ -992,11 +979,6 @@
  23.421  
  23.422  (* propositions and bindings *)
  23.423  
  23.424 -(* CB: an internal (Int) locale element was either imported or included,
  23.425 -   an external (Ext) element appears directly in the locale. *)
  23.426 -
  23.427 -datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
  23.428 -
  23.429  (* flatten (ids, expr) normalises expr (which is either a locale
  23.430     expression or a single context element) wrt.
  23.431     to the list ids of already accumulated identifiers.
  23.432 @@ -1248,27 +1230,28 @@
  23.433  end;
  23.434  
  23.435  
  23.436 -(* facts *)
  23.437 +(* facts and attributes *)
  23.438  
  23.439  local
  23.440  
  23.441 -fun prep_name ctxt (name, atts) =
  23.442 +fun prep_name ctxt name =
  23.443    (* CB: reject qualified theorem names in locale declarations *)
  23.444    if NameSpace.is_qualified name then
  23.445      raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
  23.446 -  else (name, atts);
  23.447 +  else name;
  23.448  
  23.449 -fun prep_facts _ _ (Int elem) = elem
  23.450 -  | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes
  23.451 -  | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms)
  23.452 -  | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs)
  23.453 -  | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) =>
  23.454 -      (prep_name ctxt a, map (apfst (get ctxt)) bs)));
  23.455 +fun prep_facts _ _ ctxt (Int elem) =
  23.456 +      map_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
  23.457 +  | prep_facts get intern ctxt (Ext elem) = elem |> map_elem
  23.458 +     {var = I, typ = I, term = I,
  23.459 +      name = prep_name ctxt,
  23.460 +      fact = get ctxt,
  23.461 +      attrib = Args.assignable o intern (ProofContext.sign_of ctxt)};
  23.462  
  23.463  in
  23.464  
  23.465 -fun get_facts x = prep_facts ProofContext.get_thms x;
  23.466 -fun get_facts_i x = prep_facts (K I) x;
  23.467 +fun read_facts x = prep_facts ProofContext.get_thms Attrib.intern_src x;
  23.468 +fun cert_facts x = prep_facts (K I) (K I) x;
  23.469  
  23.470  end;
  23.471  
  23.472 @@ -1312,8 +1295,8 @@
  23.473      ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), (cstmt, concl))
  23.474    end;
  23.475  
  23.476 -val gen_context = prep_context_statement intern_expr read_elemss get_facts;
  23.477 -val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i;
  23.478 +val gen_context = prep_context_statement intern_expr read_elemss read_facts;
  23.479 +val gen_context_i = prep_context_statement (K I) cert_elemss cert_facts;
  23.480  
  23.481  fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
  23.482    let
  23.483 @@ -1453,6 +1436,12 @@
  23.484  		  (map (Thm.assume o cert o inst_term Tenv') hyps))
  23.485  	  end;
  23.486  
  23.487 +    val inst_type' = inst_type Tenv';
  23.488 +
  23.489 +    val inst_term' = Term.subst_atomic
  23.490 +        (map (pairself term_of) ((cparams' @ cdefined') ~~ (cargs @ cdefining)))
  23.491 +      o inst_term Tenv';
  23.492 +
  23.493      fun inst_thm' thm =
  23.494        let
  23.495          (* not all axs are normally applicable *)
  23.496 @@ -1479,7 +1468,12 @@
  23.497  			  else inst_thm
  23.498                    in implies_elim_list th (map mk hyps)
  23.499                    end;
  23.500 -      in thm''' end;
  23.501 +      in thm''' end
  23.502 +      handle THM (msg, n, thms) => error ("Exception THM " ^
  23.503 +        string_of_int n ^ " raised\n" ^
  23.504 +	  "Note: instantiate does not support old-style locales \
  23.505 +          \declared with (open)\n" ^ msg ^ "\n" ^
  23.506 +	cat_lines (map string_of_thm thms));
  23.507  
  23.508      val prefix_fact =
  23.509        if prfx = "" then I
  23.510 @@ -1489,15 +1483,12 @@
  23.511      fun inst_elem (ctxt, (Ext _)) = ctxt
  23.512        | inst_elem (ctxt, (Int (Notes facts))) =
  23.513                (* instantiate fact *)
  23.514 -          let (* extract context attributes *)
  23.515 -              val (Notes facts) = map_attrib_element_i snd (Notes facts);
  23.516 +          let
  23.517 +              val facts = facts |> map_attrib_facts
  23.518 +                (Attrib.context_attribute_i ctxt o
  23.519 +                  Args.map_values I inst_type' inst_term' inst_thm');
  23.520                val facts' =
  23.521                  map (apsnd (map (apfst (map inst_thm')))) facts
  23.522 -		handle THM (msg, n, thms) => error ("Exception THM " ^
  23.523 -		  string_of_int n ^ " raised\n" ^
  23.524 -		  "Note: instantiate does not support old-style locales \
  23.525 -                  \declared with (open)\n" ^ msg ^ "\n" ^
  23.526 -		  cat_lines (map string_of_thm thms))
  23.527                (* rename fact *)
  23.528                val facts'' = map (apfst (apfst prefix_fact)) facts'
  23.529                (* add attributes *)
  23.530 @@ -1530,6 +1521,7 @@
  23.531      val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
  23.532      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
  23.533      val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
  23.534 +    val prt_atts = Args.pretty_attribs ctxt;
  23.535  
  23.536      fun prt_syn syn =
  23.537        let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
  23.538 @@ -1538,19 +1530,28 @@
  23.539            prt_typ T :: Pretty.brk 1 :: prt_syn syn)
  23.540        | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
  23.541  
  23.542 -    fun prt_name "" = [Pretty.brk 1]
  23.543 -      | prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1];
  23.544 -    fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts));
  23.545 -    fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]);
  23.546 -    fun prt_fact ((a, _), ths) = Pretty.block
  23.547 -      (prt_name a @ Pretty.breaks (map prt_thm (List.concat (map fst ths))));
  23.548 +    fun prt_name name = Pretty.str (ProofContext.cond_extern ctxt name);
  23.549 +    fun prt_name_atts (name, atts) =
  23.550 +      if name = "" andalso null atts then []
  23.551 +      else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))];
  23.552 +
  23.553 +    fun prt_asm (a, ts) =
  23.554 +      Pretty.block (Pretty.breaks (prt_name_atts a @ map (prt_term o fst) ts));
  23.555 +    fun prt_def (a, (t, _)) =
  23.556 +      Pretty.block (Pretty.breaks (prt_name_atts a @ [prt_term t]));
  23.557 +
  23.558 +    fun prt_fact (ths, []) = map prt_thm ths
  23.559 +      | prt_fact (ths, atts) =
  23.560 +          Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts;
  23.561 +    fun prt_note (a, ths) =
  23.562 +      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a :: map prt_fact ths)));
  23.563  
  23.564      fun items _ [] = []
  23.565        | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items "  and" xs;
  23.566      fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
  23.567        | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
  23.568        | prt_elem (Defines defs) = items "defines" (map prt_def defs)
  23.569 -      | prt_elem (Notes facts) = items "notes" (map prt_fact facts);
  23.570 +      | prt_elem (Notes facts) = items "notes" (map prt_note facts);
  23.571    in
  23.572      Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
  23.573      |> Pretty.writeln
  23.574 @@ -1645,8 +1646,8 @@
  23.575          val ids' = map (apsnd vinst_names) ids;
  23.576          val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
  23.577          val args' = map (fn ((n, atts), [(ths, [])]) =>
  23.578 -            ((if prfx = "" orelse n = "" then ""
  23.579 -              else NameSpace.pack [prfx, n], map fst atts @ atts2),
  23.580 +            ((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n],
  23.581 +              map (Attrib.global_attribute_i thy) (atts @ atts2)),
  23.582               [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sign (inst, tinst)) ths, [])]))
  23.583            args;
  23.584        in
  23.585 @@ -1656,8 +1657,7 @@
  23.586  
  23.587  
  23.588  fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
  23.589 -  | smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc;
  23.590 -  (* CB: only used in Proof.finish_global. *)
  23.591 +  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
  23.592  
  23.593  end;
  23.594  
  23.595 @@ -1668,54 +1668,48 @@
  23.596  fun put_facts loc args thy =
  23.597    let
  23.598      val {predicate, import, elems, params} = the_locale thy loc;
  23.599 -    val note = Notes (map (fn ((a, more_atts), th_atts) =>
  23.600 -      ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
  23.601 -  in thy |> put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())],
  23.602 -    params = params} end;
  23.603 +    val note = Notes (map (fn ((a, atts), bs) =>
  23.604 +      ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args);
  23.605 +  in
  23.606 +    thy |> put_locale loc {predicate = predicate, import = import,
  23.607 +      elems = elems @ [(note, stamp ())], params = params}
  23.608 +  end;
  23.609  
  23.610  (* add theorem to locale and theory,
  23.611     base for theorems (in loc) and declare (in loc) *)
  23.612  
  23.613 -fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
  23.614 +fun gen_note_thmss prep_locale prep_facts kind raw_loc args thy =
  23.615    let
  23.616      val thy_ctxt = ProofContext.init thy;
  23.617      val loc = prep_locale (Theory.sign_of thy) raw_loc;
  23.618 -    val (_, (stmt, _), loc_ctxt, _, _) =
  23.619 -      cert_context_statement (SOME loc) [] [] thy_ctxt;
  23.620 -    val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
  23.621 -    (* convert multi attributes to context attributes for
  23.622 -       ProofContext.note_thmss_i *)
  23.623 -    val args'' = args
  23.624 -          |> map (apfst (apsnd (map snd)))
  23.625 -          |> map (apsnd (map (apsnd (map snd))));
  23.626 +    val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
  23.627      val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
  23.628 -    val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args'' loc_ctxt));
  23.629 -    val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
  23.630 +
  23.631 +    val (args', facts) = #2 (activate_note prep_facts (loc_ctxt, args));
  23.632 +    val facts' =
  23.633 +      map (rpair [] o #1 o #1) args' ~~
  23.634 +      map (single o Thm.no_attributes o map export o #2) facts;
  23.635    in
  23.636      thy
  23.637 -    |> put_facts loc args
  23.638 -    |> note_thmss_registrations kind loc args
  23.639 -    |> note_thmss_qualified kind loc args'
  23.640 +    |> put_facts loc args'
  23.641 +    |> note_thmss_registrations kind loc args'
  23.642 +    |> note_thmss_qualified kind loc facts'
  23.643    end;
  23.644  
  23.645  in
  23.646  
  23.647 -(* CB: note_thmss(_i) is the base for the Isar commands
  23.648 -   "theorems (in loc)" and "declare (in loc)". *)
  23.649 -
  23.650 -val note_thmss = gen_note_thmss intern ProofContext.get_thms;
  23.651 -val note_thmss_i = gen_note_thmss (K I) (K I);
  23.652 -
  23.653 -(* CB: only used in Proof.finish_global. *)
  23.654 +val note_thmss = gen_note_thmss intern read_facts;
  23.655 +val note_thmss_i = gen_note_thmss (K I) cert_facts;
  23.656  
  23.657  fun add_thmss kind loc args (thy, ctxt) =
  23.658    let
  23.659 -    val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
  23.660 -    val thy' = put_facts loc args' thy;
  23.661 -    val thy'' = note_thmss_registrations kind loc args' thy';
  23.662 -    val (ctxt', (_, facts')) =
  23.663 -      activate_facts (K I) (ctxt, [((("", []), []), [Notes args'])]);
  23.664 -  in ((thy'', ctxt'), facts') end;
  23.665 +    val (ctxt', (args', facts)) = activate_note cert_facts
  23.666 +      (ctxt, args |> map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])));
  23.667 +    val thy' =
  23.668 +      thy
  23.669 +      |> put_facts loc args'
  23.670 +      |> note_thmss_registrations kind loc args';
  23.671 +  in ((thy', ctxt'), facts) end;
  23.672  
  23.673  end;
  23.674  
  23.675 @@ -1803,18 +1797,18 @@
  23.676     - notes elements are lifted
  23.677  *)
  23.678  
  23.679 -fun change_elem _ (axms, Assumes asms) =
  23.680 +fun change_elem (axms, Assumes asms) =
  23.681        apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
  23.682          let val (ps,qs) = splitAt(length spec, axs)
  23.683          in (qs, (a, [(ps, [])])) end))
  23.684 -  | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts))
  23.685 -  | change_elem _ e = e;
  23.686 +  | change_elem e = e;
  23.687  
  23.688  (* CB: changes only "new" elems, these have identifier ("", _). *)
  23.689  
  23.690  fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
  23.691    (fn (axms, (id as ("", _), es)) =>
  23.692 -    foldl_map (change_elem (Drule.satisfy_hyps axioms)) (axms, es) |> apsnd (pair id)
  23.693 +    foldl_map change_elem (axms, map (map_values I I (Drule.satisfy_hyps axioms)) es)
  23.694 +    |> apsnd (pair id)
  23.695    | x => x) |> #2;
  23.696  
  23.697  in
  23.698 @@ -1944,14 +1938,13 @@
  23.699  fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt
  23.700    | activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt
  23.701    | activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt
  23.702 -  | activate_facts_elem note_thmss which
  23.703 +  | activate_facts_elem note_thmss attrib
  23.704          disch (prfx, atts) (thy_ctxt, Notes facts) =
  23.705        let
  23.706 -        (* extract theory or context attributes *)
  23.707 -        val (Notes facts) = map_attrib_element_i which (Notes facts);
  23.708 -        (* add attributes from registration *)
  23.709 -        val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
  23.710 -        (* discharge hyps  *)
  23.711 +        val reg_atts = map (attrib thy_ctxt) atts;
  23.712 +        val facts = map_attrib_facts (attrib thy_ctxt) facts;
  23.713 +        val facts' = map (apfst (apsnd (fn a => a @ reg_atts))) facts;
  23.714 +        (* discharge hyps *)
  23.715          val facts'' = map (apsnd (map (apfst (map disch)))) facts';
  23.716          (* prefix names *)
  23.717          val facts''' = map (apfst (apfst (fn name =>
  23.718 @@ -1961,25 +1954,25 @@
  23.719          fst (note_thmss prfx facts''' thy_ctxt)
  23.720        end;
  23.721  
  23.722 -fun activate_facts_elems get_reg note_thmss which
  23.723 +fun activate_facts_elems get_reg note_thmss attrib
  23.724          disch (thy_ctxt, (id, elems)) =
  23.725        let
  23.726          val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
  23.727            handle Option => error ("(internal) unknown registration of " ^
  23.728              quote (fst id) ^ " while activating facts.");
  23.729        in
  23.730 -        Library.foldl (activate_facts_elem note_thmss which
  23.731 +        Library.foldl (activate_facts_elem note_thmss attrib
  23.732            disch (prfx, atts2)) (thy_ctxt, elems)
  23.733        end;
  23.734  
  23.735 -fun gen_activate_facts_elemss get_reg note_thmss which standard
  23.736 +fun gen_activate_facts_elemss get_reg note_thmss attrib standard
  23.737          all_elemss new_elemss thy_ctxt =
  23.738        let
  23.739          val prems = List.concat (List.mapPartial (fn (id, _) =>
  23.740                Option.map snd (get_reg thy_ctxt id)
  23.741                  handle Option => error ("(internal) unknown registration of " ^
  23.742                    quote (fst id) ^ " while activating facts.")) all_elemss);
  23.743 -      in Library.foldl (activate_facts_elems get_reg note_thmss which
  23.744 +      in Library.foldl (activate_facts_elems get_reg note_thmss attrib
  23.745          (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
  23.746  
  23.747  val global_activate_facts_elemss = gen_activate_facts_elemss
  23.748 @@ -1987,11 +1980,11 @@
  23.749          get_global_registration thy (name, map Logic.varify ps))
  23.750        (fn prfx => PureThy.note_thmss_accesses_i (global_accesses prfx)
  23.751          (Drule.kind ""))
  23.752 -      fst Drule.standard;
  23.753 +      Attrib.global_attribute_i Drule.standard;
  23.754  val local_activate_facts_elemss = gen_activate_facts_elemss
  23.755        get_local_registration
  23.756        (fn prfx => ProofContext.note_thmss_accesses_i (local_accesses prfx))
  23.757 -      snd I;
  23.758 +      Attrib.context_attribute_i I;
  23.759  
  23.760  fun gen_prep_registration mk_ctxt is_local read_terms test_reg put_reg activate
  23.761      attn expr insts thy_ctxt =
  23.762 @@ -2072,9 +2065,12 @@
  23.763      (* remove fragments already registered with theory or context *)
  23.764      val new_inst_elemss = List.filter (fn (id, _) =>
  23.765            not (test_reg thy_ctxt id)) inst_elemss;
  23.766 +    val new_ids = map #1 new_inst_elemss;
  23.767  
  23.768      val propss = extract_asms_elemss new_inst_elemss;
  23.769  
  23.770 +    val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
  23.771 +    val attn' = apsnd (map (bind_attrib o Attrib.intern_src sign)) attn;
  23.772  
  23.773      (** add registrations to theory or context,
  23.774          without theorems, these are added after the proof **)
  23.775 @@ -2083,7 +2079,7 @@
  23.776         registration. *)
  23.777  
  23.778      val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
  23.779 -          put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss);
  23.780 +          put_reg id attn' thy_ctxt) (thy_ctxt, new_inst_elemss);
  23.781  
  23.782    in (thy_ctxt', propss, activate inst_elemss new_inst_elemss) end;
  23.783  
    24.1 --- a/src/Pure/Isar/method.ML	Wed Apr 13 09:48:41 2005 +0200
    24.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 13 18:34:22 2005 +0200
    24.3 @@ -15,6 +15,7 @@
    24.4  signature METHOD =
    24.5  sig
    24.6    include BASIC_METHOD
    24.7 +  type src
    24.8    val trace: Proof.context -> thm list -> unit
    24.9    val RAW_METHOD: (thm list -> tactic) -> Proof.method
   24.10    val RAW_METHOD_CASES:
   24.11 @@ -48,37 +49,37 @@
   24.12    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
   24.13    val tactic: string -> Proof.context -> Proof.method
   24.14    exception METHOD_FAIL of (string * Position.T) * exn
   24.15 -  val method: theory -> Args.src -> Proof.context -> Proof.method
   24.16 -  val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string
   24.17 +  val method: theory -> src -> Proof.context -> Proof.method
   24.18 +  val add_method: bstring * (src -> Proof.context -> Proof.method) * string
   24.19      -> theory -> theory
   24.20 -  val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
   24.21 +  val add_methods: (bstring * (src -> Proof.context -> Proof.method) * string) list
   24.22      -> theory -> theory
   24.23    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
   24.24 -    Args.src -> Proof.context -> Proof.context * 'a
   24.25 +    src -> Proof.context -> Proof.context * 'a
   24.26    val simple_args: (Args.T list -> 'a * Args.T list)
   24.27 -    -> ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
   24.28 -  val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
   24.29 -  val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
   24.30 +    -> ('a -> Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
   24.31 +  val ctxt_args: (Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
   24.32 +  val no_args: Proof.method -> src -> Proof.context -> Proof.method
   24.33    type modifier
   24.34    val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
   24.35      (Args.T list -> modifier * Args.T list) list ->
   24.36 -    ('a -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
   24.37 +    ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
   24.38    val bang_sectioned_args:
   24.39      (Args.T list -> modifier * Args.T list) list ->
   24.40 -    (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
   24.41 +    (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
   24.42    val bang_sectioned_args':
   24.43      (Args.T list -> modifier * Args.T list) list ->
   24.44      (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
   24.45 -    ('a -> thm list -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
   24.46 +    ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
   24.47    val only_sectioned_args:
   24.48      (Args.T list -> modifier * Args.T list) list ->
   24.49 -    (Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
   24.50 -  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
   24.51 -  val thms_args: (thm list -> 'a) -> Args.src -> Proof.context -> 'a
   24.52 -  val thm_args: (thm -> 'a) -> Args.src -> Proof.context -> 'a
   24.53 +    (Proof.context -> 'a) -> src -> Proof.context -> 'a
   24.54 +  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
   24.55 +  val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
   24.56 +  val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
   24.57    datatype text =
   24.58      Basic of (Proof.context -> Proof.method) |
   24.59 -    Source of Args.src |
   24.60 +    Source of src |
   24.61      Then of text list |
   24.62      Orelse of text list |
   24.63      Try of text |
   24.64 @@ -107,19 +108,21 @@
   24.65      theory * ((string * string) * (string * thm list) list)
   24.66    val global_done_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
   24.67    val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
   24.68 -    -> Args.src -> Proof.context -> Proof.method
   24.69 +    -> src -> Proof.context -> Proof.method
   24.70    val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
   24.71 -    -> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   24.72 +    -> ('a -> int -> tactic) -> src -> Proof.context -> Proof.method
   24.73    val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
   24.74 -    -> Args.src -> Proof.context -> Proof.method
   24.75 +    -> src -> Proof.context -> Proof.method
   24.76    val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
   24.77 -    -> (Proof.context -> 'a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   24.78 +    -> (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> Proof.method
   24.79    val setup: (theory -> theory) list
   24.80  end;
   24.81  
   24.82  structure Method: METHOD =
   24.83  struct
   24.84  
   24.85 +type src = Args.src;
   24.86 +
   24.87  
   24.88  (** proof methods **)
   24.89  
   24.90 @@ -374,7 +377,7 @@
   24.91                | some => some)
   24.92            | types' xi = types xi;
   24.93          fun internal x = isSome (types' (x, ~1));
   24.94 -        val used = Term.add_term_tvarnames (Thm.prop_of st $ Thm.prop_of thm, []);
   24.95 +        val used = Drule.add_used thm (Drule.add_used st []);
   24.96          val (ts, envT) =
   24.97            ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
   24.98          val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
   24.99 @@ -505,7 +508,7 @@
  24.100    val name = "Isar/methods";
  24.101    type T =
  24.102      {space: NameSpace.T,
  24.103 -     meths: (((Args.src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
  24.104 +     meths: (((src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
  24.105  
  24.106    val empty = {space = NameSpace.empty, meths = Symtab.empty};
  24.107    val copy = I;
  24.108 @@ -692,7 +695,7 @@
  24.109  
  24.110  datatype text =
  24.111    Basic of (Proof.context -> Proof.method) |
  24.112 -  Source of Args.src |
  24.113 +  Source of src |
  24.114    Then of text list |
  24.115    Orelse of text list |
  24.116    Try of text |
    25.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Apr 13 09:48:41 2005 +0200
    25.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Apr 13 18:34:22 2005 +0200
    25.3 @@ -14,9 +14,7 @@
    25.4    val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
    25.5    val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
    25.6    val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
    25.7 -  val $$$ : string -> token list -> string * token list
    25.8 -  val semicolon: token list -> string * token list
    25.9 -  val underscore: token list -> string * token list
   25.10 +  val not_eof: token list -> token * token list
   25.11    val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
   25.12    val command: token list -> string * token list
   25.13    val keyword: token list -> string * token list
   25.14 @@ -31,7 +29,10 @@
   25.15    val verbatim: token list -> string * token list
   25.16    val sync: token list -> string * token list
   25.17    val eof: token list -> string * token list
   25.18 -  val not_eof: token list -> token * token list
   25.19 +  val $$$ : string -> token list -> string * token list
   25.20 +  val semicolon: token list -> string * token list
   25.21 +  val underscore: token list -> string * token list
   25.22 +  val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
   25.23    val opt_unit: token list -> unit * token list
   25.24    val opt_keyword: string -> token list -> bool * token list
   25.25    val nat: token list -> int * token list
   25.26 @@ -45,7 +46,6 @@
   25.27    val xname: token list -> xstring * token list
   25.28    val text: token list -> string * token list
   25.29    val path: token list -> Path.T * token list
   25.30 -  val uname: token list -> string option * token list
   25.31    val sort: token list -> string * token list
   25.32    val arity: token list -> (string list * string) * token list
   25.33    val type_args: token list -> string list * token list
   25.34 @@ -61,19 +61,19 @@
   25.35    val propp: token list -> (string * (string list * string list)) * token list
   25.36    val termp: token list -> (string * string list) * token list
   25.37    val arguments: token list -> Args.T list * token list
   25.38 -  val attribs: token list -> Args.src list * token list
   25.39 -  val opt_attribs: token list -> Args.src list * token list
   25.40 -  val thm_name: string -> token list -> (bstring * Args.src list) * token list
   25.41 -  val opt_thm_name: string -> token list -> (bstring * Args.src list) * token list
   25.42 -  val spec_name: token list -> ((bstring * string) * Args.src list) * token list
   25.43 -  val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
   25.44 -  val xthm: token list -> (thmref * Args.src list) * token list
   25.45 -  val xthms1: token list -> (thmref * Args.src list) list * token list
   25.46 +  val attribs: token list -> Attrib.src list * token list
   25.47 +  val opt_attribs: token list -> Attrib.src list * token list
   25.48 +  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
   25.49 +  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
   25.50 +  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
   25.51 +  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
   25.52 +  val xthm: token list -> (thmref * Attrib.src list) * token list
   25.53 +  val xthms1: token list -> (thmref * Attrib.src list) list * token list
   25.54    val locale_target: token list -> xstring option * token list
   25.55    val locale_expr: token list -> Locale.expr * token list
   25.56    val locale_keyword: token list -> string * token list
   25.57 -  val locale_element: token list -> Args.src Locale.element * token list
   25.58 -  val locale_elem_or_expr: token list -> Args.src Locale.element Locale.elem_expr * token list
   25.59 +  val locale_element: token list -> Locale.element * token list
   25.60 +  val locale_elem_or_expr: token list -> Locale.element Locale.elem_expr * token list
   25.61    val method: token list -> Method.text * token list
   25.62  end;
   25.63  
   25.64 @@ -122,8 +122,9 @@
   25.65  
   25.66  (* tokens *)
   25.67  
   25.68 -fun position scan =
   25.69 -  (Scan.ahead (Scan.one T.not_eof) >> T.position_of) -- scan >> Library.swap;
   25.70 +val not_eof = Scan.one T.not_eof;
   25.71 +
   25.72 +fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
   25.73  
   25.74  fun kind k =
   25.75    group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);
   25.76 @@ -148,13 +149,12 @@
   25.77  
   25.78  val semicolon = $$$ ";";
   25.79  
   25.80 +val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
   25.81  val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
   25.82 -val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
   25.83 +fun maybe scan = underscore >> K NONE || scan >> SOME;
   25.84  
   25.85  val nat = number >> (#1 o Library.read_int o Symbol.explode);
   25.86  
   25.87 -val not_eof = Scan.one T.not_eof;
   25.88 -
   25.89  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   25.90  
   25.91  fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
   25.92 @@ -179,8 +179,6 @@
   25.93  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
   25.94  val path = group "file name/path specification" name >> Path.unpack;
   25.95  
   25.96 -val uname = underscore >> K NONE || name >> SOME;
   25.97 -
   25.98  
   25.99  (* sorts and arities *)
  25.100  
  25.101 @@ -265,13 +263,13 @@
  25.102  fun atom_arg is_symid blk =
  25.103    group "argument"
  25.104      (position (short_ident || long_ident || sym_ident || term_var ||
  25.105 -        type_ident || type_var || number) >> Args.ident ||
  25.106 -      position (keyword_symid is_symid) >> Args.keyword ||
  25.107 -      position (string || verbatim) >> Args.string ||
  25.108 -      position (if blk then $$$ "," else Scan.fail) >> Args.keyword);
  25.109 +        type_ident || type_var || number) >> Args.mk_ident ||
  25.110 +      position (keyword_symid is_symid) >> Args.mk_keyword ||
  25.111 +      position (string || verbatim) >> Args.mk_string ||
  25.112 +      position (if blk then $$$ "," else Scan.fail) >> Args.mk_keyword);
  25.113  
  25.114  fun paren_args l r scan = position ($$$ l) -- !!! (scan true -- position ($$$ r))
  25.115 -  >> (fn (x, (ys, z)) => Args.keyword x :: ys @ [Args.keyword z]);
  25.116 +  >> (fn (x, (ys, z)) => Args.mk_keyword x :: ys @ [Args.mk_keyword z]);
  25.117  
  25.118  fun args is_symid blk x = Scan.optional (args1 is_symid blk) [] x
  25.119  and args1 is_symid blk x =
  25.120 @@ -297,8 +295,9 @@
  25.121  val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
  25.122  
  25.123  val thm_sel = $$$ "(" |-- list1
  25.124 -  (   nat --| minus -- nat >> op upto
  25.125 -   || nat >> single) --| $$$ ")" >> List.concat;
  25.126 + (nat --| minus -- nat >> PureThy.FromTo ||
  25.127 +  nat --| minus >> PureThy.From ||
  25.128 +  nat >> PureThy.Single) --| $$$ ")";
  25.129  
  25.130  val xthm = xname -- Scan.option thm_sel -- opt_attribs;
  25.131  val xthms1 = Scan.repeat1 xthm;
  25.132 @@ -325,7 +324,7 @@
  25.133    scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
  25.134  
  25.135  fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
  25.136 -and expr1 x = (expr2 -- Scan.repeat1 uname >> Locale.Rename || expr2) x
  25.137 +and expr1 x = (expr2 -- Scan.repeat1 (maybe name) >> Locale.Rename || expr2) x
  25.138  and expr0 x = (plus1 expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
  25.139  
  25.140  in
    26.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 13 09:48:41 2005 +0200
    26.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 13 18:34:22 2005 +0200
    26.3 @@ -90,19 +90,17 @@
    26.4    val def: string -> context attribute list -> string *  (string * string list) -> state -> state
    26.5    val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
    26.6    val invoke_case: string * string option list * context attribute list -> state -> state
    26.7 -  val multi_theorem:
    26.8 -    string -> (theory -> theory) ->
    26.9 +  val multi_theorem: string -> (theory -> theory) ->
   26.10      (cterm list -> context -> context -> thm -> thm) ->
   26.11 -    (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
   26.12 -    -> bstring * theory attribute list -> Locale.multi_attribute Locale.element Locale.elem_expr list
   26.13 +    (xstring * (Attrib.src list * Attrib.src list list)) option ->
   26.14 +    bstring * theory attribute list -> Locale.element Locale.elem_expr list
   26.15      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
   26.16      -> theory -> state
   26.17 -  val multi_theorem_i:
   26.18 -    string -> (theory -> theory)  ->
   26.19 +  val multi_theorem_i: string -> (theory -> theory) ->
   26.20      (cterm list -> context -> context -> thm -> thm) ->
   26.21 -    (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
   26.22 +    (string * (Attrib.src list * Attrib.src list list)) option
   26.23      -> bstring * theory attribute list
   26.24 -    -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
   26.25 +    -> Locale.element_i Locale.elem_expr list
   26.26      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
   26.27      -> theory -> state
   26.28    val chain: state -> state
   26.29 @@ -119,12 +117,6 @@
   26.30    val have_i: (state -> state Seq.seq) -> bool
   26.31      -> ((string * context attribute list) * (term * (term list * term list)) list) list
   26.32      -> state -> state
   26.33 -  val interpret: (context -> context) -> (state -> state Seq.seq) -> bool
   26.34 -    -> ((string * context attribute list) * (string * (string list * string list)) list) list
   26.35 -    -> state -> state
   26.36 -  val interpret_i: (context -> context) -> (state -> state Seq.seq) -> bool
   26.37 -    -> ((string * context attribute list) * (term * (term list * term list)) list) list
   26.38 -    -> state -> state
   26.39    val at_bottom: state -> bool
   26.40    val local_qed: (state -> state Seq.seq)
   26.41      -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
   26.42 @@ -136,8 +128,6 @@
   26.43    val next_block: state -> state
   26.44    val thisN: string
   26.45    val call_atp: bool ref;
   26.46 -
   26.47 -
   26.48  end;
   26.49  
   26.50  structure Proof: PROOF =
   26.51 @@ -153,33 +143,15 @@
   26.52  
   26.53  (* type goal *)
   26.54  
   26.55 -(* CB: four kinds of Isar goals are distinguished:
   26.56 -   - Theorem: global goal in a theory, corresponds to Isar commands theorem,
   26.57 -     lemma and corollary,
   26.58 -   - Have: local goal in a proof, Isar command have
   26.59 -   - Show: local goal in a proof, Isar command show
   26.60 -   - Interpret: local goal in a proof, Isar command interpret
   26.61 -*)
   26.62 -
   26.63  datatype kind =
   26.64    Theorem of {kind: string,
   26.65      theory_spec: (bstring * theory attribute list) * theory attribute list list,
   26.66 -    locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option,
   26.67 -    view: cterm list * cterm list, (* target view and includes view *)
   26.68 -    thy_mod: theory -> theory,     (* used in finish_global to modify final
   26.69 -                                      theory, normally set to I; used by
   26.70 -                                      registration command to activate
   26.71 -                                      registrations *)
   26.72 -    export: cterm list -> context -> context -> thm -> thm } |
   26.73 +    locale_spec: (string * (Attrib.src list * Attrib.src list list)) option,
   26.74 +    view: cterm list * cterm list,  (* target view and includes view *)
   26.75 +    export: cterm list -> context -> context -> thm -> thm} |
   26.76                                     (* exporter to be used in finish_global *)
   26.77    Show of context attribute list list |
   26.78 -  Have of context attribute list list |
   26.79 -  Interpret of {attss: context attribute list list,
   26.80 -    ctxt_mod: context -> context}; (* used in finish_local to modify final
   26.81 -                                      context *)
   26.82 -
   26.83 -(* CB: this function prints the goal kind (Isar command), name and target in
   26.84 -   the proof state *)
   26.85 +  Have of context attribute list list;
   26.86  
   26.87  fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
   26.88          locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a)
   26.89 @@ -187,8 +159,7 @@
   26.90          locale_spec = SOME (name, _), ...}) =
   26.91        s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
   26.92    | kind_name _ (Show _) = "show"
   26.93 -  | kind_name _ (Have _) = "have"
   26.94 -  | kind_name _ (Interpret _) = "interpret";
   26.95 +  | kind_name _ (Have _) = "have";
   26.96  
   26.97  type goal =
   26.98   (kind *             (*result kind*)
   26.99 @@ -211,11 +182,13 @@
  26.100     {context: context,
  26.101      facts: thm list option,
  26.102      mode: mode,
  26.103 -    goal: (goal * ((state -> state Seq.seq) * bool)) option}
  26.104 +    goal: (goal * (after_qed * bool)) option}
  26.105  and state =
  26.106    State of
  26.107      node *              (*current*)
  26.108 -    node list;          (*parents wrt. block structure*)
  26.109 +    node list           (*parents wrt. block structure*)
  26.110 +and after_qed =
  26.111 +  AfterQed of (state -> state Seq.seq) * (theory -> theory);
  26.112  
  26.113  fun make_node (context, facts, mode, goal) =
  26.114    Node {context = context, facts = facts, mode = mode, goal = goal};
  26.115 @@ -658,7 +631,8 @@
  26.116  
  26.117  (* locale instantiation *)
  26.118  
  26.119 -fun instantiate_locale (loc_name, prfx_attribs) state = let
  26.120 +fun instantiate_locale (loc_name, prfx_attribs) state =
  26.121 +  let
  26.122      val facts = if is_chain state then get_facts state else NONE;
  26.123    in
  26.124      state
  26.125 @@ -668,6 +642,7 @@
  26.126      |> map_context (Locale.instantiate loc_name prfx_attribs facts)
  26.127    end;
  26.128  
  26.129 +
  26.130  (* fix *)
  26.131  
  26.132  fun gen_fix f xs state =
  26.133 @@ -774,6 +749,9 @@
  26.134        |> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
  26.135      val sign' = sign_of state';
  26.136  
  26.137 +    val AfterQed (after_local, after_global) = after_qed;
  26.138 +    val after_qed' = AfterQed (after_local o map_context gen_binds, after_global);
  26.139 +
  26.140      val props = List.concat propss;
  26.141      val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
  26.142      val goal = Drule.mk_triv_goal cprop;
  26.143 @@ -789,8 +767,7 @@
  26.144        commas (map (ProofContext.string_of_term (context_of state')) vars));
  26.145      state'
  26.146      |> map_context (autofix props)
  26.147 -    |> put_goal (SOME (((kind, names, propss), ([], goal)),
  26.148 -      (after_qed o map_context gen_binds, pr)))
  26.149 +    |> put_goal (SOME (((kind, names, propss), ([], goal)), (after_qed', pr)))
  26.150      |> map_context (ProofContext.add_cases
  26.151       (if length props = 1 then
  26.152        RuleCases.make true NONE (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
  26.153 @@ -802,7 +779,7 @@
  26.154    end;
  26.155  
  26.156  (*global goals*)
  26.157 -fun global_goal prep kind thy_mod export raw_locale a elems concl thy =
  26.158 +fun global_goal prep kind after_global export raw_locale a elems concl thy =
  26.159    let
  26.160      val init = init_state thy;
  26.161      val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
  26.162 @@ -813,16 +790,14 @@
  26.163      |> map_context (K locale_ctxt)
  26.164      |> open_block
  26.165      |> map_context (K elems_ctxt)
  26.166 -(* CB: elems_ctxt is an extension of locale_ctxt, see prep_context_statement
  26.167 -   in locale.ML, naming there: ctxt and import_ctxt. *)
  26.168      |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
  26.169        (Theorem {kind = kind,
  26.170          theory_spec = (a, map (snd o fst) concl),
  26.171          locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
  26.172          view = view,
  26.173 -        thy_mod = thy_mod,
  26.174          export = export})
  26.175 -      Seq.single true (map (fst o fst) concl) propp
  26.176 +      (AfterQed (Seq.single, after_global))
  26.177 +      true (map (fst o fst) concl) propp
  26.178    end;
  26.179  
  26.180  val multi_theorem = global_goal Locale.read_context_statement;
  26.181 @@ -830,10 +805,10 @@
  26.182  
  26.183  
  26.184  (*local goals*)
  26.185 -fun local_goal' prepp kind (check: bool -> state -> state) f pr args int state =
  26.186 +fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state =
  26.187    state
  26.188    |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
  26.189 -    f pr (map (fst o fst) args) (map snd args)
  26.190 +    (AfterQed (after_local, I)) pr (map (fst o fst) args) (map snd args)
  26.191    |> warn_extra_tfrees state
  26.192    |> check int;
  26.193  
  26.194 @@ -843,10 +818,7 @@
  26.195  val show_i = local_goal' ProofContext.bind_propp_i Show;
  26.196  val have = local_goal ProofContext.bind_propp Have;
  26.197  val have_i = local_goal ProofContext.bind_propp_i Have;
  26.198 -fun interpret ctxt_mod = local_goal ProofContext.bind_propp
  26.199 -  (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod});
  26.200 -fun interpret_i ctxt_mod = local_goal ProofContext.bind_propp_i
  26.201 -  (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod});
  26.202 +
  26.203  
  26.204  
  26.205  (** conclusions **)
  26.206 @@ -884,7 +856,8 @@
  26.207  
  26.208  fun finish_local (print_result, print_rule) state =
  26.209    let
  26.210 -    val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (after_qed, pr))) = current_goal state;
  26.211 +    val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (after_local, _), pr))) =
  26.212 +      current_goal state;
  26.213      val outer_state = state |> close_block;
  26.214      val outer_ctxt = context_of outer_state;
  26.215  
  26.216 @@ -894,30 +867,21 @@
  26.217        results |> map (ProofContext.export false goal_ctxt outer_ctxt)
  26.218        |> Seq.commute |> Seq.map (Library.unflat tss);
  26.219  
  26.220 -    val (attss, opt_solve, ctxt_mod) =
  26.221 +    val (attss, opt_solve) =
  26.222        (case kind of
  26.223          Show attss => (attss,
  26.224 -          export_goals goal_ctxt (if pr then print_rule else (K (K ())))
  26.225 -            results, I)
  26.226 -      | Have attss => (attss, Seq.single, I)
  26.227 -      | Interpret {attss, ctxt_mod} => (attss, Seq.single, ctxt_mod)
  26.228 +          export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results)
  26.229 +      | Have attss => (attss, Seq.single)
  26.230        | _ => err_malformed "finish_local" state);
  26.231    in
  26.232      conditional pr (fn () => print_result goal_ctxt
  26.233        (kind_name (sign_of state) kind, names ~~ Library.unflat tss results));
  26.234      outer_state
  26.235      |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
  26.236 -(* original version
  26.237      |> (fn st => Seq.map (fn res =>
  26.238 -      note_thmss_i ((names ~~ attss) ~~
  26.239 -          map (single o Thm.no_attributes) res) st) resultq)
  26.240 -*)
  26.241 -    |> (fn st => Seq.map (fn res =>
  26.242 -      st |> note_thmss_i ((names ~~ attss) ~~
  26.243 -              map (single o Thm.no_attributes) res)
  26.244 -         |> map_context ctxt_mod) resultq)
  26.245 +      note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
  26.246      |> (Seq.flat o Seq.map opt_solve)
  26.247 -    |> (Seq.flat o Seq.map after_qed)
  26.248 +    |> (Seq.flat o Seq.map after_local)
  26.249    end;
  26.250  
  26.251  fun local_qed finalize print state =
  26.252 @@ -931,11 +895,14 @@
  26.253  
  26.254  fun finish_global state =
  26.255    let
  26.256 -    val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
  26.257 +    val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (_, after_global), _))) =
  26.258 +      current_goal state;
  26.259      val locale_ctxt = context_of (state |> close_block);
  26.260      val theory_ctxt = context_of (state |> close_block |> close_block);
  26.261 -    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod, export} =
  26.262 +    val {kind = k, theory_spec = ((name, atts), attss),
  26.263 +        locale_spec, view = (target_view, elems_view), export} =
  26.264        (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
  26.265 +    val locale_name = Option.map fst locale_spec;
  26.266  
  26.267      val ts = List.concat tss;
  26.268      val locale_results = map (export elems_view goal_ctxt locale_ctxt)
  26.269 @@ -956,12 +923,12 @@
  26.270              if name = "" andalso null loc_atts then thy'
  26.271              else (thy', ctxt')
  26.272                |> (#1 o #1 o Locale.add_thmss k loc [((name, List.concat (map #2 res)), loc_atts)])))
  26.273 -      |> Locale.smart_note_thmss k locale_spec
  26.274 +      |> Locale.smart_note_thmss k locale_name
  26.275          ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
  26.276        |> (fn (thy, res) => (thy, res)
  26.277 -          |>> (#1 o Locale.smart_note_thmss k locale_spec
  26.278 +          |>> (#1 o Locale.smart_note_thmss k locale_name
  26.279              [((name, atts), [(List.concat (map #2 res), [])])]));
  26.280 -  in (thy_mod theory', ((k, name), results')) end;
  26.281 +  in (after_global theory', ((k, name), results')) end;
  26.282  
  26.283  
  26.284  (*note: clients should inspect first result only, as backtracking may destroy theory*)
    27.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 13 09:48:41 2005 +0200
    27.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 13 18:34:22 2005 +0200
    27.3 @@ -8,7 +8,7 @@
    27.4  (*Jia: changed: datatype context
    27.5         affected files:  make_context, map_context, init, put_data, add_syntax, map_defaults, del_bind, upd_bind, qualified, hide_thms, put_thms, reset_thms, gen_assms, map_fixes, add_cases
    27.6  
    27.7 -       added: put_delta, get_delta 
    27.8 +       added: put_delta, get_delta
    27.9         06/01/05
   27.10  *)
   27.11  
   27.12 @@ -62,6 +62,8 @@
   27.13    val cert_prop_pats: context -> term list -> term list
   27.14    val declare_term: term -> context -> context
   27.15    val declare_terms: term list -> context -> context
   27.16 +  val read_tyname: context -> string -> typ
   27.17 +  val read_const: context -> string -> term
   27.18    val warn_extra_tfrees: context -> context -> context
   27.19    val generalize: context -> context -> term list -> term list
   27.20    val find_free: term -> string -> term option
   27.21 @@ -163,7 +165,7 @@
   27.22    val setup: (theory -> theory) list
   27.23  
   27.24    val get_delta: context -> Object.T Symtab.table (* Jia: (claset, simpset) *)
   27.25 -  val put_delta: Object.T Symtab.table -> context -> context 
   27.26 +  val put_delta: Object.T Symtab.table -> context -> context
   27.27    val get_delta_count_incr: context -> int
   27.28  
   27.29  end;
   27.30 @@ -648,10 +650,7 @@
   27.31  
   27.32  in
   27.33  
   27.34 -(* CB: for attribute where.  See attrib.ML. *)
   27.35  val read_termTs           = gen_read' (read_def_termTs false) (apfst o map) false false false;
   27.36 -
   27.37 -(* CB: for rule_tac etc.  See method.ML. *)
   27.38  val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false false true;
   27.39  
   27.40  fun read_term_pats T ctxt =
   27.41 @@ -743,6 +742,19 @@
   27.42  end;
   27.43  
   27.44  
   27.45 +(* type and constant names *)
   27.46 +
   27.47 +fun read_tyname ctxt c =
   27.48 +  if c mem_string used_types ctxt then
   27.49 +    TFree (c, getOpt (def_sort ctxt (c, ~1), Sign.defaultS (sign_of ctxt)))
   27.50 +  else Sign.read_tyname (sign_of ctxt) c;
   27.51 +
   27.52 +fun read_const ctxt c =
   27.53 +  (case lookup_skolem ctxt c of
   27.54 +    SOME c' => Free (c', dummyT)
   27.55 +  | NONE => Sign.read_const (sign_of ctxt) c);
   27.56 +
   27.57 +
   27.58  
   27.59  (** Hindley-Milner polymorphism **)
   27.60  
    28.1 --- a/src/Pure/axclass.ML	Wed Apr 13 09:48:41 2005 +0200
    28.2 +++ b/src/Pure/axclass.ML	Wed Apr 13 18:34:22 2005 +0200
    28.3 @@ -11,7 +11,7 @@
    28.4    val print_axclasses: theory -> unit
    28.5    val add_classrel_thms: thm list -> theory -> theory
    28.6    val add_arity_thms: thm list -> theory -> theory
    28.7 -  val add_axclass: bclass * xclass list -> ((bstring * string) * Args.src list) list
    28.8 +  val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list
    28.9      -> theory -> theory * {intro: thm, axioms: thm list}
   28.10    val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
   28.11      -> theory -> theory * {intro: thm, axioms: thm list}
    29.1 --- a/src/Pure/pure_thy.ML	Wed Apr 13 09:48:41 2005 +0200
    29.2 +++ b/src/Pure/pure_thy.ML	Wed Apr 13 18:34:22 2005 +0200
    29.3 @@ -24,6 +24,7 @@
    29.4  signature PURE_THY =
    29.5  sig
    29.6    include BASIC_PURE_THY
    29.7 +  datatype interval = FromTo of int * int | From of int | Single of int
    29.8    val get_thm_closure: theory -> thmref -> thm
    29.9    val get_thms_closure: theory -> thmref -> thm list
   29.10    val single_thm: string -> thm list -> thm
   29.11 @@ -145,20 +146,42 @@
   29.12  
   29.13  (** retrieve theorems **)
   29.14  
   29.15 -type thmref = xstring * int list option;
   29.16 -
   29.17 -(* selections *)
   29.18 -
   29.19  fun the_thms _ (SOME thms) = thms
   29.20    | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
   29.21  
   29.22  fun single_thm _ [thm] = thm
   29.23    | single_thm name _ = error ("Single theorem expected " ^ quote name);
   29.24  
   29.25 -fun select_thm (s, NONE) xs = xs
   29.26 -  | select_thm (s, SOME is) xs = map
   29.27 -      (fn i => (if i < 1 then raise Subscript else List.nth (xs, i-1)) handle Subscript =>
   29.28 -         error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;
   29.29 +
   29.30 +(* selections *)
   29.31 +
   29.32 +datatype interval =
   29.33 +  FromTo of int * int |
   29.34 +  From of int |
   29.35 +  Single of int;
   29.36 +
   29.37 +type thmref = xstring * interval list option;
   29.38 +
   29.39 +local
   29.40 +
   29.41 +fun interval _ (FromTo (i, j)) = i upto j
   29.42 +  | interval n (From i) = i upto n
   29.43 +  | interval _ (Single i) = [i];
   29.44 +
   29.45 +fun select name thms n i =
   29.46 +  if i < 1 orelse i > n then
   29.47 +    error ("Bad subscript " ^ string_of_int i ^ " for " ^
   29.48 +      quote name ^ " (length " ^ string_of_int n ^ ")")
   29.49 +  else List.nth (thms, i - 1);
   29.50 +
   29.51 +in
   29.52 +
   29.53 +fun select_thm (_, NONE) thms = thms
   29.54 +  | select_thm (name, SOME is) thms =
   29.55 +      let val n = length thms
   29.56 +      in map (select name thms n) (List.concat (map (interval n) is)) end;
   29.57 +
   29.58 +end;
   29.59  
   29.60  
   29.61  (* get_thm(s)_closure -- statically scoped versions *)
   29.62 @@ -222,6 +245,7 @@
   29.63    thms_containing thy (consts, []) |> map #2 |> List.concat
   29.64    |> map (fn th => (Thm.name_of_thm th, th))
   29.65  
   29.66 +
   29.67  (* intro/elim theorems *)
   29.68  
   29.69  (* intro: given a goal state, find a suitable intro rule for some subgoal *)
    30.1 --- a/src/Pure/sign.ML	Wed Apr 13 09:48:41 2005 +0200
    30.2 +++ b/src/Pure/sign.ML	Wed Apr 13 18:34:22 2005 +0200
    30.3 @@ -42,6 +42,8 @@
    30.4    val is_stale: sg -> bool
    30.5    val syn_of: sg -> Syntax.syntax
    30.6    val const_type: sg -> string -> typ option
    30.7 +  val declared_tyname: sg -> string -> bool
    30.8 +  val declared_const: sg -> string -> bool
    30.9    val classes: sg -> class list
   30.10    val defaultS: sg -> sort
   30.11    val subsort: sg -> sort * sort -> bool
   30.12 @@ -93,14 +95,14 @@
   30.13    val certify_sort: sg -> sort -> sort
   30.14    val certify_typ: sg -> typ -> typ
   30.15    val certify_typ_raw: sg -> typ -> typ
   30.16 -  val certify_tyname: sg -> string -> string
   30.17 -  val certify_const: sg -> string -> string
   30.18    val certify_term: Pretty.pp -> sg -> term -> term * typ * int
   30.19    val read_sort: sg -> string -> sort
   30.20    val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
   30.21    val read_typ: sg * (indexname -> sort option) -> string -> typ
   30.22    val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   30.23    val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   30.24 +  val read_tyname: sg -> string -> typ
   30.25 +  val read_const: sg -> string -> term
   30.26    val inst_typ_tvars: sg -> (indexname * typ) list -> typ -> typ
   30.27    val inst_term_tvars: sg -> (indexname * typ) list -> term -> term
   30.28    val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
   30.29 @@ -164,7 +166,7 @@
   30.30    val merge: sg * sg -> sg
   30.31    val copy: sg -> sg
   30.32    val prep_ext: sg -> sg
   30.33 -  val nontriv_merge: sg * sg -> sg
   30.34 +  val prep_ext_merge: sg list -> sg
   30.35  end;
   30.36  
   30.37  signature PRIVATE_SIGN =
   30.38 @@ -234,6 +236,9 @@
   30.39  fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
   30.40  fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
   30.41  
   30.42 +fun declared_tyname sg c = isSome (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
   30.43 +fun declared_const sg c = isSome (const_type sg c);
   30.44 +
   30.45  
   30.46  (* id and self *)
   30.47  
   30.48 @@ -266,22 +271,15 @@
   30.49    fun subset_stamp ([], ys) = true
   30.50      | subset_stamp (x :: xs, ys) =
   30.51          mem_stamp (x, ys) andalso subset_stamp (xs, ys);
   30.52 -
   30.53 -  (*fast partial test*)
   30.54 -  fun fast_sub ([]: string ref list, _) = true
   30.55 -    | fast_sub (_, []) = false
   30.56 -    | fast_sub (x :: xs, y :: ys) =
   30.57 -        if x = y then fast_sub (xs, ys)
   30.58 -        else fast_sub (x :: xs, ys);
   30.59  in
   30.60    fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
   30.61      (check_stale sg1; check_stale sg2; id1 = id2);
   30.62  
   30.63    fun subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   30.64 -    eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
   30.65 +    eq_sg (sg1, sg2) orelse mem_stamp (hd s1, s2);
   30.66  
   30.67 -  fun fast_subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   30.68 -    eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
   30.69 +  fun subsig_internal (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   30.70 +    eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
   30.71  end;
   30.72  
   30.73  
   30.74 @@ -703,14 +701,6 @@
   30.75  val certify_typ = Type.cert_typ o tsig_of;
   30.76  val certify_typ_raw = Type.cert_typ_raw o tsig_of;
   30.77  
   30.78 -fun certify_tyname sg c =
   30.79 -  if isSome (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
   30.80 -  else raise TYPE ("Undeclared type constructor: " ^ quote c, [], []);
   30.81 -
   30.82 -fun certify_const sg c =
   30.83 -  if isSome (const_type sg c) then c
   30.84 -  else raise TYPE ("Undeclared constant: " ^ quote c, [], []);
   30.85 -
   30.86  
   30.87  (* certify_term *)
   30.88  
   30.89 @@ -822,6 +812,22 @@
   30.90  end;
   30.91  
   30.92  
   30.93 +(* type and constant names *)
   30.94 +
   30.95 +fun read_tyname sg raw_c =
   30.96 +  let val c = intern_tycon sg raw_c in
   30.97 +    (case Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c) of
   30.98 +      SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
   30.99 +    | NONE => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
  30.100 +  end;
  30.101 +
  30.102 +fun read_const sg raw_c =
  30.103 +  let val c = intern_const sg raw_c in
  30.104 +    if isSome (const_type sg c) then Const (c, dummyT)
  30.105 +    else raise TYPE ("Undeclared constant: " ^ quote c, [], [])
  30.106 +  end;
  30.107 +
  30.108 +
  30.109  
  30.110  (** instantiation **)
  30.111  
  30.112 @@ -991,7 +997,7 @@
  30.113    error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
  30.114  
  30.115  
  30.116 -fun read_const sg syn tsig (path, spaces) (c, ty_src, mx) =
  30.117 +fun read_cnst sg syn tsig (path, spaces) (c, ty_src, mx) =
  30.118    (c, rd_raw_typ (make_syntax sg syn) tsig spaces (K NONE) ty_src, mx)
  30.119      handle ERROR => err_in_const (const_name path c mx);
  30.120  
  30.121 @@ -1015,11 +1021,11 @@
  30.122    end;
  30.123  
  30.124  fun ext_consts_i x = ext_cnsts no_read false Syntax.default_mode x;
  30.125 -fun ext_consts x = ext_cnsts read_const false Syntax.default_mode x;
  30.126 +fun ext_consts x = ext_cnsts read_cnst false Syntax.default_mode x;
  30.127  fun ext_syntax_i x = ext_cnsts no_read true Syntax.default_mode x;
  30.128 -fun ext_syntax x = ext_cnsts read_const true Syntax.default_mode x;
  30.129 +fun ext_syntax x = ext_cnsts read_cnst true Syntax.default_mode x;
  30.130  fun ext_modesyntax_i x y (prmode, consts) = ext_cnsts no_read true prmode x y consts;
  30.131 -fun ext_modesyntax x y (prmode, consts) = ext_cnsts read_const true prmode x y consts;
  30.132 +fun ext_modesyntax x y (prmode, consts) = ext_cnsts read_cnst true prmode x y consts;
  30.133  
  30.134  
  30.135  (* add type classes *)
  30.136 @@ -1198,9 +1204,7 @@
  30.137  
  30.138  fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
  30.139          sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
  30.140 -      if fast_subsig (sg2, sg1) then sgr1
  30.141 -      else if fast_subsig (sg1, sg2) then sgr2
  30.142 -      else if subsig (sg2, sg1) then sgr1
  30.143 +      if subsig (sg2, sg1) then sgr1
  30.144        else if subsig (sg1, sg2) then sgr2
  30.145        else (merge_stamps s1 s2; (*check for different versions*)
  30.146          raise TERM ("Attempt to do non-trivial merge of signatures", []))
  30.147 @@ -1209,16 +1213,17 @@
  30.148  val merge = deref o merge_refs o pairself self_ref;
  30.149  
  30.150  
  30.151 -(* non-trivial merge *)              (*exception TERM/ERROR*)
  30.152 +(* merge_list *)              (*exception TERM/ERROR*)
  30.153 +
  30.154 +local
  30.155  
  30.156  fun nontriv_merge (sg1, sg2) =
  30.157 -  if subsig (sg2, sg1) then sg1
  30.158 -  else if subsig (sg1, sg2) then sg2
  30.159 -  else if is_draft sg1 orelse is_draft sg2 then
  30.160 -    raise TERM ("Attempt to merge draft signatures", [])
  30.161 -  else if exists_stamp PureN sg1 andalso exists_stamp CPureN sg2 orelse
  30.162 -      exists_stamp CPureN sg1 andalso exists_stamp PureN sg2 then
  30.163 -    raise TERM ("Cannot merge Pure and CPure signatures", [])
  30.164 +  if subsig_internal (sg2, sg1) then sg1
  30.165 +  else if subsig_internal (sg1, sg2) then sg2
  30.166 +  else
  30.167 +    if exists_stamp PureN sg1 andalso exists_stamp CPureN sg2 orelse
  30.168 +      exists_stamp CPureN sg1 andalso exists_stamp PureN sg2
  30.169 +    then error "Cannot merge Pure and CPure signatures"
  30.170    else
  30.171      let
  30.172        val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
  30.173 @@ -1253,4 +1258,18 @@
  30.174          path, spaces, data, stamps);
  30.175      in self_ref := sign; syn_of sign; sign end;
  30.176  
  30.177 +in
  30.178 +
  30.179 +fun prep_ext_merge sgs =
  30.180 +  if null sgs then
  30.181 +    error "Merge: no parent theories"
  30.182 +  else if exists is_draft sgs then
  30.183 +    error "Attempt to merge draft theories"
  30.184 +  else
  30.185 +    Library.foldl nontriv_merge (hd sgs, tl sgs)
  30.186 +    |> prep_ext
  30.187 +    |> add_path "/";
  30.188 +
  30.189  end;
  30.190 +
  30.191 +end;
    31.1 --- a/src/Pure/theory.ML	Wed Apr 13 09:48:41 2005 +0200
    31.2 +++ b/src/Pure/theory.ML	Wed Apr 13 18:34:22 2005 +0200
    31.3 @@ -540,43 +540,32 @@
    31.4  
    31.5  (** merge theories **)          (*exception ERROR*)
    31.6  
    31.7 -fun merge_sign (sg, thy) =
    31.8 -  Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
    31.9 -
   31.10  (*merge list of theories from left to right, preparing extend*)
   31.11  fun prep_ext_merge thys =
   31.12 -  if null thys then
   31.13 -    error "Merge: no parent theories"
   31.14 -  else if exists is_draft thys then
   31.15 -    error "Attempt to merge draft theories"
   31.16 -  else
   31.17 -    let
   31.18 -      val sign' =
   31.19 -        Library.foldl merge_sign (sign_of (hd thys), tl thys)
   31.20 -        |> Sign.prep_ext
   31.21 -        |> Sign.add_path "/";
   31.22 +  let
   31.23 +    val sign' = Sign.prep_ext_merge (map sign_of thys)
   31.24  
   31.25 -      val depss = map (#const_deps o rep_theory) thys;
   31.26 -      val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
   31.27 -        handle Graph.CYCLES namess => error (cycle_msg namess);
   31.28 +    val depss = map (#const_deps o rep_theory) thys;
   31.29 +    val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
   31.30 +      handle Graph.CYCLES namess => error (cycle_msg namess);
   31.31 +
   31.32 +    val final_constss = map (#final_consts o rep_theory) thys;
   31.33 +    val final_consts' =
   31.34 +      Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
   31.35 +    val axioms' = Symtab.empty;
   31.36  
   31.37 -      val final_constss = map (#final_consts o rep_theory) thys;
   31.38 -      val final_consts' = Library.foldl (Symtab.join (merge_final sign')) (hd final_constss,
   31.39 -								   tl final_constss);
   31.40 -      val axioms' = Symtab.empty;
   31.41 +    fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   31.42 +    val oracles' =
   31.43 +      Symtab.make (gen_distinct eq_ora
   31.44 +        (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
   31.45 +      handle Symtab.DUPS names => err_dup_oras names;
   31.46  
   31.47 -      fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   31.48 -      val oracles' =
   31.49 -        Symtab.make (gen_distinct eq_ora
   31.50 -          (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
   31.51 -        handle Symtab.DUPS names => err_dup_oras names;
   31.52 -
   31.53 -      val parents' = gen_distinct eq_thy thys;
   31.54 -      val ancestors' =
   31.55 -        gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   31.56 -    in
   31.57 -      make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
   31.58 -    end;
   31.59 +    val parents' = gen_distinct eq_thy thys;
   31.60 +    val ancestors' =
   31.61 +      gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   31.62 +  in
   31.63 +    make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
   31.64 +  end;
   31.65  
   31.66  
   31.67  end;
    32.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Apr 13 09:48:41 2005 +0200
    32.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Apr 13 18:34:22 2005 +0200
    32.3 @@ -36,8 +36,8 @@
    32.4    val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
    32.5      thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    32.6    val add_datatype: string * string list -> (string * string list * mixfix) list list ->
    32.7 -    (thmref * Args.src list) list * (thmref * Args.src list) list *
    32.8 -    (thmref * Args.src list) list -> theory -> theory * inductive_result * datatype_result
    32.9 +    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
   32.10 +    (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
   32.11  end;
   32.12  
   32.13  functor Add_datatype_def_Fun
    33.1 --- a/src/ZF/Tools/ind_cases.ML	Wed Apr 13 09:48:41 2005 +0200
    33.2 +++ b/src/ZF/Tools/ind_cases.ML	Wed Apr 13 18:34:22 2005 +0200
    33.3 @@ -8,7 +8,7 @@
    33.4  signature IND_CASES =
    33.5  sig
    33.6    val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
    33.7 -  val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
    33.8 +  val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    33.9    val setup: (theory -> theory) list
   33.10  end;
   33.11  
    34.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 09:48:41 2005 +0200
    34.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:34:22 2005 +0200
    34.3 @@ -13,8 +13,8 @@
    34.4    val induct_tac: string -> int -> tactic
    34.5    val exhaust_tac: string -> int -> tactic
    34.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
    34.7 -  val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
    34.8 -    (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
    34.9 +  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
   34.10 +    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
   34.11    val setup: (theory -> theory) list
   34.12  end;
   34.13  
    35.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Apr 13 09:48:41 2005 +0200
    35.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Apr 13 18:34:22 2005 +0200
    35.3 @@ -34,9 +34,9 @@
    35.4    val add_inductive_x: string list * string -> ((bstring * string) * theory attribute list) list
    35.5      -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
    35.6    val add_inductive: string list * string ->
    35.7 -    ((bstring * string) * Args.src list) list ->
    35.8 -    (thmref * Args.src list) list * (thmref * Args.src list) list *
    35.9 -    (thmref * Args.src list) list * (thmref * Args.src list) list ->
   35.10 +    ((bstring * string) * Attrib.src list) list ->
   35.11 +    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
   35.12 +    (thmref * Attrib.src list) list * (thmref * Attrib.src list) list ->
   35.13      theory -> theory * inductive_result
   35.14  end;
   35.15  
    36.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Apr 13 09:48:41 2005 +0200
    36.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Apr 13 18:34:22 2005 +0200
    36.3 @@ -10,7 +10,7 @@
    36.4  signature PRIMREC_PACKAGE =
    36.5  sig
    36.6    val quiet_mode: bool ref
    36.7 -  val add_primrec: ((bstring * string) * Args.src list) list -> theory -> theory * thm list
    36.8 +  val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
    36.9    val add_primrec_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
   36.10  end;
   36.11