Merge
authorpaulson <lp15@cam.ac.uk>
Sat Apr 11 16:19:14 2015 +0100 (2015-04-11)
changeset 6001805d4dce039c6
parent 60017 b785d6d06430
parent 60010 5fe58ca9cf40
child 60019 4dda564e8a5d
Merge
     1.1 --- a/Admin/Release/build_library	Sat Apr 11 11:56:40 2015 +0100
     1.2 +++ b/Admin/Release/build_library	Sat Apr 11 16:19:14 2015 +0100
     1.3 @@ -75,7 +75,6 @@
     1.4  cd *
     1.5  ISABELLE_NAME="$(basename "$PWD")"
     1.6  
     1.7 -echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
     1.8  echo "ISABELLE_FULL_TEST=true" >> etc/settings
     1.9  
    1.10  echo -n > src/Doc/ROOT
     2.1 --- a/Admin/components/bundled-windows	Sat Apr 11 11:56:40 2015 +0100
     2.2 +++ b/Admin/components/bundled-windows	Sat Apr 11 16:19:14 2015 +0100
     2.3 @@ -1,3 +1,3 @@
     2.4  #additional components to be bundled for release
     2.5 -cygwin-20140813
     2.6 +cygwin-20150410
     2.7  windows_app-20131201
     3.1 --- a/Admin/components/components.sha1	Sat Apr 11 11:56:40 2015 +0100
     3.2 +++ b/Admin/components/components.sha1	Sat Apr 11 16:19:14 2015 +0100
     3.3 @@ -14,6 +14,7 @@
     3.4  8e562dfe57a2f894f9461f4addedb88afa108152  cygwin-20140725.tar.gz
     3.5  238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf  cygwin-20140813.tar.gz
     3.6  629b8fbe35952d1551cd2a7ff08db697f6dff870  cygwin-20141024.tar.gz
     3.7 +ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c  cygwin-20150410.tar.gz
     3.8  0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
     3.9  2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
    3.10  e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
     4.1 --- a/Admin/isatest/settings/mac-poly-M2-alternative	Sat Apr 11 11:56:40 2015 +0100
     4.2 +++ b/Admin/isatest/settings/mac-poly-M2-alternative	Sat Apr 11 16:19:14 2015 +0100
     4.3 @@ -30,6 +30,3 @@
     4.4  ISABELLE_FULL_TEST=true
     4.5  
     4.6  ISABELLE_GHC=ghc
     4.7 -
     4.8 -Z3_NON_COMMERCIAL="yes"
     4.9 -
     5.1 --- a/Admin/isatest/settings/mac-poly-M4	Sat Apr 11 11:56:40 2015 +0100
     5.2 +++ b/Admin/isatest/settings/mac-poly-M4	Sat Apr 11 16:19:14 2015 +0100
     5.3 @@ -35,6 +35,3 @@
     5.4  ISABELLE_POLYML="$ML_HOME/poly"
     5.5  #ISABELLE_SCALA="$SCALA_HOME/bin"
     5.6  ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
     5.7 -
     5.8 -Z3_NON_COMMERCIAL="yes"
     5.9 -
     6.1 --- a/Admin/isatest/settings/mac-poly-M8	Sat Apr 11 11:56:40 2015 +0100
     6.2 +++ b/Admin/isatest/settings/mac-poly-M8	Sat Apr 11 16:19:14 2015 +0100
     6.3 @@ -35,6 +35,3 @@
     6.4  ISABELLE_POLYML="$ML_HOME/poly"
     6.5  #ISABELLE_SCALA="$SCALA_HOME/bin"
     6.6  ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
     6.7 -
     6.8 -Z3_NON_COMMERCIAL="yes"
     6.9 -
     7.1 --- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty	Sat Apr 11 11:56:40 2015 +0100
     7.2 +++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty	Sat Apr 11 16:19:14 2015 +0100
     7.3 @@ -27,6 +27,3 @@
     7.4  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
     7.5  
     7.6  ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty"
     7.7 -
     7.8 -Z3_NON_COMMERCIAL="yes"
     7.9 -
     8.1 --- a/Admin/isatest/settings/mac-poly-M8-skip_proofs	Sat Apr 11 11:56:40 2015 +0100
     8.2 +++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs	Sat Apr 11 16:19:14 2015 +0100
     8.3 @@ -27,6 +27,3 @@
     8.4  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
     8.5  
     8.6  ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
     8.7 -
     8.8 -Z3_NON_COMMERCIAL="yes"
     8.9 -
     9.1 --- a/Admin/lib/Tools/makedist_cygwin	Sat Apr 11 11:56:40 2015 +0100
     9.2 +++ b/Admin/lib/Tools/makedist_cygwin	Sat Apr 11 16:19:14 2015 +0100
     9.3 @@ -4,7 +4,7 @@
     9.4  
     9.5  ## global parameters
     9.6  
     9.7 -CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2014"
     9.8 +CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2015"
     9.9  
    9.10  
    9.11  ## diagnostics
    9.12 @@ -55,7 +55,7 @@
    9.13    --site "$CYGWIN_MIRROR" --no-verify \
    9.14    --local-package-dir 'C:\temp' \
    9.15    --root "$(cygpath -w "$TARGET")" \
    9.16 -  --packages libgmp3,perl,perl_vendor,rlwrap,unzip,vim \
    9.17 +  --packages perl,perl-libwww-perl,rlwrap,unzip,vim \
    9.18    --no-shortcuts --no-startmenu --no-desktop --quiet-mode
    9.19  
    9.20  [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
    9.21 @@ -65,7 +65,7 @@
    9.22  
    9.23  for NAME in hosts protocols services networks passwd group
    9.24  do
    9.25 -  rm "$TARGET/etc/$NAME"
    9.26 +  rm -f "$TARGET/etc/$NAME"
    9.27  done
    9.28  
    9.29  ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
    9.30 @@ -77,4 +77,3 @@
    9.31  
    9.32  DATE=$(date +%Y%m%d)
    9.33  tar -C "$TARGET/.." -cz -f "cygwin-${DATE}.tar.gz" cygwin
    9.34 -
    10.1 --- a/Admin/mira.py	Sat Apr 11 11:56:40 2015 +0100
    10.2 +++ b/Admin/mira.py	Sat Apr 11 16:19:14 2015 +0100
    10.3 @@ -24,7 +24,6 @@
    10.4  
    10.5      # patch settings
    10.6      extra_settings = '''
    10.7 -Z3_NON_COMMERCIAL="yes"
    10.8  
    10.9  init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
   10.10  init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
    11.1 --- a/NEWS	Sat Apr 11 11:56:40 2015 +0100
    11.2 +++ b/NEWS	Sat Apr 11 16:19:14 2015 +0100
    11.3 @@ -1,8 +1,11 @@
    11.4  Isabelle NEWS -- history of user-relevant changes
    11.5  =================================================
    11.6  
    11.7 -New in this Isabelle version
    11.8 -----------------------------
    11.9 +(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
   11.10 +
   11.11 +
   11.12 +New in Isabelle2015 (May 2015)
   11.13 +------------------------------
   11.14  
   11.15  *** General ***
   11.16  
   11.17 @@ -54,9 +57,6 @@
   11.18  
   11.19  *** Prover IDE -- Isabelle/Scala/jEdit ***
   11.20  
   11.21 -* Old graph browser (Java/AWT 1.1) is superseded by improved graphview
   11.22 -panel, which also produces PDF output without external tools.
   11.23 -
   11.24  * Improved folding mode "isabelle" based on Isar syntax. Alternatively,
   11.25  the "sidekick" mode may be used for document structure.
   11.26  
   11.27 @@ -74,12 +74,12 @@
   11.28  * Less waste of vertical space via negative line spacing (see Global
   11.29  Options / Text Area).
   11.30  
   11.31 +* Old graph browser (Java/AWT 1.1) is superseded by improved graphview
   11.32 +panel, which also produces PDF output without external tools.
   11.33 +
   11.34  
   11.35  *** Document preparation ***
   11.36  
   11.37 -* Discontinued obsolete option "document_graph": session_graph.pdf is
   11.38 -produced unconditionally for HTML browser_info and PDF-LaTeX document.
   11.39 -
   11.40  * Document markup commands 'chapter', 'section', 'subsection',
   11.41  'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
   11.42  context, even before the initial 'theory' command. Obsolete proof
   11.43 @@ -89,6 +89,17 @@
   11.44  should be replaced by 'chapter', 'section' etc. (using "isabelle
   11.45  update_header"). Minor INCOMPATIBILITY.
   11.46  
   11.47 +* Official support for "tt" style variants, via \isatt{...} or
   11.48 +\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
   11.49 +verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
   11.50 +as argument to other macros (such as footnotes).
   11.51 +
   11.52 +* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
   11.53 +style.
   11.54 +
   11.55 +* Discontinued obsolete option "document_graph": session_graph.pdf is
   11.56 +produced unconditionally for HTML browser_info and PDF-LaTeX document.
   11.57 +
   11.58  * Diagnostic commands and document markup commands within a proof do not
   11.59  affect the command tag for output. Thus commands like 'thm' are subject
   11.60  to proof document structure, and no longer "stick out" accidentally.
   11.61 @@ -103,21 +114,9 @@
   11.62  antiquotations need to observe the margin explicitly according to
   11.63  Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
   11.64  
   11.65 -* Official support for "tt" style variants, via \isatt{...} or
   11.66 -\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
   11.67 -verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
   11.68 -as argument to other macros (such as footnotes).
   11.69 -
   11.70 -* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
   11.71 -style.
   11.72 -
   11.73  
   11.74  *** Pure ***
   11.75  
   11.76 -* Explicit instantiation via attributes "where", "of", and proof methods
   11.77 -"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
   11.78 -("_") that stand for anonymous local variables.
   11.79 -
   11.80  * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
   11.81  etc.) allow an optional context of local variables ('for' declaration):
   11.82  these variables become schematic in the instantiated theorem; this
   11.83 @@ -127,18 +126,22 @@
   11.84  declare rule_insts_schematic = true temporarily and update to use local
   11.85  variable declarations or dummy patterns instead.
   11.86  
   11.87 +* Explicit instantiation via attributes "where", "of", and proof methods
   11.88 +"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
   11.89 +("_") that stand for anonymous local variables.
   11.90 +
   11.91  * Generated schematic variables in standard format of exported facts are
   11.92  incremented to avoid material in the proof context. Rare
   11.93  INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
   11.94  different index.
   11.95  
   11.96 -* Command "class_deps" takes optional sort arguments constraining
   11.97 -the search space.
   11.98 -
   11.99 -* Lexical separation of signed and unsigend numerals: categories "num"
  11.100 -and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
  11.101 -of numeral signs, particulary in expressions involving infix syntax like
  11.102 -"(- 1) ^ n".
  11.103 +* Command "class_deps" takes optional sort arguments to constrain then
  11.104 +resulting class hierarchy.
  11.105 +
  11.106 +* Lexical separation of signed and unsigned numerals: categories "num"
  11.107 +and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
  11.108 +of numeral signs, particularly in expressions involving infix syntax
  11.109 +like "(- 1) ^ n".
  11.110  
  11.111  * Old inner token category "xnum" has been discontinued.  Potential
  11.112  INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
  11.113 @@ -147,88 +150,6 @@
  11.114  
  11.115  *** HOL ***
  11.116  
  11.117 -* Given up separate type class no_zero_divisors in favour of fully
  11.118 -algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
  11.119 -
  11.120 -* Class linordered_semidom really requires no zero divisors.
  11.121 -INCOMPATIBILITY.
  11.122 -
  11.123 -* Classes division_ring, field and linordered_field always demand
  11.124 -"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
  11.125 -field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
  11.126 -
  11.127 -* Type classes cancel_ab_semigroup_add / cancel_monoid_add specify
  11.128 -explicit additive inverse operation. INCOMPATIBILITY.
  11.129 -
  11.130 -* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
  11.131 -single-step rewriting with subterm selection based on patterns.
  11.132 -
  11.133 -* The functions "sin" and "cos" are now defined for any
  11.134 -"'{real_normed_algebra_1,banach}" type, so in particular on "real" and
  11.135 -"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
  11.136 -needed.
  11.137 -
  11.138 -* New library of properties of the complex transcendental functions sin,
  11.139 -cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
  11.140 -
  11.141 -* The factorial function, "fact", now has type "nat => 'a" (of a sort
  11.142 -that admits numeric types including nat, int, real and complex.
  11.143 -INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
  11.144 -constraint, and the combination "real (fact k)" is likely to be
  11.145 -unsatisfactory. If a type conversion is still necessary, then use
  11.146 -"of_nat (fact k)" or "real_of_nat (fact k)".
  11.147 -
  11.148 -* Removed functions "natfloor" and "natceiling", use "nat o floor" and
  11.149 -"nat o ceiling" instead. A few of the lemmas have been retained and
  11.150 -adapted: in their names "natfloor"/"natceiling" has been replaced by
  11.151 -"nat_floor"/"nat_ceiling".
  11.152 -
  11.153 -* Qualified some duplicated fact names required for boostrapping the
  11.154 -type class hierarchy:
  11.155 -  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
  11.156 -  field_inverse_zero ~> inverse_zero
  11.157 -  field_divide_inverse ~> divide_inverse
  11.158 -  field_inverse ~> left_inverse
  11.159 -Minor INCOMPATIBILITY.
  11.160 -
  11.161 -* Eliminated fact duplicates:
  11.162 -  mult_less_imp_less_right ~> mult_right_less_imp_less
  11.163 -  mult_less_imp_less_left ~> mult_left_less_imp_less
  11.164 -Minor INCOMPATIBILITY.
  11.165 -
  11.166 -* Fact consolidation: even_less_0_iff is subsumed by
  11.167 -double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
  11.168 -
  11.169 -* Add NO_MATCH-simproc, allows to check for syntactic non-equality.
  11.170 -
  11.171 -* Generalized and consolidated some theorems concerning divsibility:
  11.172 -  dvd_reduce ~> dvd_add_triv_right_iff
  11.173 -  dvd_plus_eq_right ~> dvd_add_right_iff
  11.174 -  dvd_plus_eq_left ~> dvd_add_left_iff
  11.175 -Minor INCOMPATIBILITY.
  11.176 -
  11.177 -* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
  11.178 -and part of theory Main.
  11.179 -  even_def ~> even_iff_mod_2_eq_zero
  11.180 -INCOMPATIBILITY.
  11.181 -
  11.182 -* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
  11.183 -INCOMPATIBILITY.
  11.184 -
  11.185 -* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
  11.186 -non-termination in case of distributing a division. With this change
  11.187 -field_simps is in some cases slightly less powerful, if it fails try to
  11.188 -add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
  11.189 -
  11.190 -* Bootstrap of listsum as special case of abstract product over lists.
  11.191 -Fact rename:
  11.192 -    listsum_def ~> listsum.eq_foldr
  11.193 -INCOMPATIBILITY.
  11.194 -
  11.195 -* Command and antiquotation "value" provide different evaluation slots
  11.196 -(again), where the previous strategy (NBE after ML) serves as default.
  11.197 -Minor INCOMPATIBILITY.
  11.198 -
  11.199  * New (co)datatype package:
  11.200    - The 'datatype_new' command has been renamed 'datatype'. The old
  11.201      command of that name is now called 'old_datatype' and is provided
  11.202 @@ -285,10 +206,8 @@
  11.203        ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
  11.204      INCOMPATIBILITY.
  11.205  
  11.206 -* Product over lists via constant "listprod".
  11.207 -
  11.208  * Nitpick:
  11.209 -  - Fixed soundness bug related to the strict and nonstrict subset
  11.210 +  - Fixed soundness bug related to the strict and non-strict subset
  11.211      operations.
  11.212  
  11.213  * Sledgehammer:
  11.214 @@ -297,7 +216,7 @@
  11.215    - Z3 is now always enabled by default, now that it is fully open
  11.216      source. The "z3_non_commercial" option is discontinued.
  11.217    - Minimization is now always enabled by default.
  11.218 -    Removed subcommand:
  11.219 +    Removed sub-command:
  11.220        min
  11.221    - Proof reconstruction, both one-liners and Isar, has been
  11.222      dramatically improved.
  11.223 @@ -318,18 +237,95 @@
  11.224    - New option 'smt_statistics' to display statistics of the new 'smt'
  11.225      method, especially runtime statistics of Z3 proof reconstruction.
  11.226  
  11.227 -* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc.
  11.228 +* Command and antiquotation "value" provide different evaluation slots
  11.229 +(again), where the previous strategy (NBE after ML) serves as default.
  11.230 +Minor INCOMPATIBILITY.
  11.231 +
  11.232 +* Add NO_MATCH-simproc, allows to check for syntactic non-equality.
  11.233 +
  11.234 +* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
  11.235 +non-termination in case of distributing a division. With this change
  11.236 +field_simps is in some cases slightly less powerful, if it fails try to
  11.237 +add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
  11.238 +
  11.239 +* Separate class no_zero_divisors has been given up in favour of fully
  11.240 +algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
  11.241 +
  11.242 +* Class linordered_semidom really requires no zero divisors.
  11.243 +INCOMPATIBILITY.
  11.244 +
  11.245 +* Classes division_ring, field and linordered_field always demand
  11.246 +"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
  11.247 +field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
  11.248 +
  11.249 +* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
  11.250 +additive inverse operation. INCOMPATIBILITY.
  11.251 +
  11.252 +* The functions "sin" and "cos" are now defined for any type of sort
  11.253 +"{real_normed_algebra_1,banach}" type, so in particular on "real" and
  11.254 +"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
  11.255 +needed.
  11.256 +
  11.257 +* New library of properties of the complex transcendental functions sin,
  11.258 +cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
  11.259 +
  11.260 +* The factorial function, "fact", now has type "nat => 'a" (of a sort
  11.261 +that admits numeric types including nat, int, real and complex.
  11.262 +INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
  11.263 +constraint, and the combination "real (fact k)" is likely to be
  11.264 +unsatisfactory. If a type conversion is still necessary, then use
  11.265 +"of_nat (fact k)" or "real_of_nat (fact k)".
  11.266 +
  11.267 +* Removed functions "natfloor" and "natceiling", use "nat o floor" and
  11.268 +"nat o ceiling" instead. A few of the lemmas have been retained and
  11.269 +adapted: in their names "natfloor"/"natceiling" has been replaced by
  11.270 +"nat_floor"/"nat_ceiling".
  11.271 +
  11.272 +* Qualified some duplicated fact names required for boostrapping the
  11.273 +type class hierarchy:
  11.274 +  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
  11.275 +  field_inverse_zero ~> inverse_zero
  11.276 +  field_divide_inverse ~> divide_inverse
  11.277 +  field_inverse ~> left_inverse
  11.278 +Minor INCOMPATIBILITY.
  11.279 +
  11.280 +* Eliminated fact duplicates:
  11.281 +  mult_less_imp_less_right ~> mult_right_less_imp_less
  11.282 +  mult_less_imp_less_left ~> mult_left_less_imp_less
  11.283 +Minor INCOMPATIBILITY.
  11.284 +
  11.285 +* Fact consolidation: even_less_0_iff is subsumed by
  11.286 +double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
  11.287 +
  11.288 +* Generalized and consolidated some theorems concerning divsibility:
  11.289 +  dvd_reduce ~> dvd_add_triv_right_iff
  11.290 +  dvd_plus_eq_right ~> dvd_add_right_iff
  11.291 +  dvd_plus_eq_left ~> dvd_add_left_iff
  11.292 +Minor INCOMPATIBILITY.
  11.293 +
  11.294 +* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
  11.295 +and part of theory Main.
  11.296 +  even_def ~> even_iff_mod_2_eq_zero
  11.297 +INCOMPATIBILITY.
  11.298 +
  11.299 +* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
  11.300 +INCOMPATIBILITY.
  11.301 +
  11.302 +* Bootstrap of listsum as special case of abstract product over lists.
  11.303 +Fact rename:
  11.304 +    listsum_def ~> listsum.eq_foldr
  11.305 +INCOMPATIBILITY.
  11.306 +
  11.307 +* Product over lists via constant "listprod".
  11.308 +
  11.309 +* Theory List: renamed drop_Suc_conv_tl and nth_drop' to
  11.310 +Cons_nth_drop_Suc.
  11.311  
  11.312  * New infrastructure for compiling, running, evaluating and testing
  11.313  generated code in target languages in HOL/Library/Code_Test. See
  11.314  HOL/Codegenerator_Test/Code_Test* for examples.
  11.315  
  11.316 -* Library/Sum_of_Squares: simplified and improved "sos" method. Always
  11.317 -use local CSDP executable, which is much faster than the NEOS server.
  11.318 -The "sos_cert" functionality is invoked as "sos" with additional
  11.319 -argument. Minor INCOMPATIBILITY.
  11.320 -
  11.321 -* Theory "Library/Multiset":
  11.322 +* Library/Multiset:
  11.323    - Introduced "replicate_mset" operation.
  11.324    - Introduced alternative characterizations of the multiset ordering in
  11.325      "Library/Multiset_Order".
  11.326 @@ -345,6 +341,8 @@
  11.327      INCOMPATIBILITY.
  11.328    - Renamed
  11.329        in_multiset_of ~> in_multiset_in_set
  11.330 +      Multiset.fold ~> fold_mset
  11.331 +      Multiset.filter ~> filter_mset
  11.332      INCOMPATIBILITY.
  11.333    - Removed mcard, is equal to size.
  11.334    - Added attributes:
  11.335 @@ -358,26 +356,37 @@
  11.336        in_Union_mset_iff [iff]
  11.337      INCOMPATIBILITY.
  11.338  
  11.339 -* HOL-Decision_Procs:
  11.340 -  - New counterexample generator quickcheck[approximation] for
  11.341 -    inequalities of transcendental functions.
  11.342 -    Uses hardware floating point arithmetic to randomly discover
  11.343 -    potential counterexamples. Counterexamples are certified with the
  11.344 -    'approximation' method.
  11.345 -    See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
  11.346 -    examples.
  11.347 +* Library/Sum_of_Squares: simplified and improved "sos" method. Always
  11.348 +use local CSDP executable, which is much faster than the NEOS server.
  11.349 +The "sos_cert" functionality is invoked as "sos" with additional
  11.350 +argument. Minor INCOMPATIBILITY.
  11.351 +
  11.352 +* HOL-Decision_Procs: New counterexample generator quickcheck
  11.353 +[approximation] for inequalities of transcendental functions. Uses
  11.354 +hardware floating point arithmetic to randomly discover potential
  11.355 +counterexamples. Counterexamples are certified with the "approximation"
  11.356 +method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
  11.357 +examples.
  11.358  
  11.359  * HOL-Probability: Reworked measurability prover
  11.360 -  - applies destructor rules repeatetly
  11.361 +  - applies destructor rules repeatedly
  11.362    - removed application splitting (replaced by destructor rule)
  11.363    - added congruence rules to rewrite measure spaces under the sets
  11.364      projection
  11.365  
  11.366 +* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
  11.367 +single-step rewriting with subterm selection based on patterns.
  11.368 +
  11.369  
  11.370  *** ML ***
  11.371  
  11.372 -* Cartouches within ML sources are turned into values of type
  11.373 -Input.source (with formal position information).
  11.374 +* Subtle change of name space policy: undeclared entries are now
  11.375 +considered inaccessible, instead of accessible via the fully-qualified
  11.376 +internal name. This mainly affects Name_Space.intern (and derivatives),
  11.377 +which may produce an unexpected Long_Name.hidden prefix. Note that
  11.378 +contemporary applications use the strict Name_Space.check (and
  11.379 +derivatives) instead, which is not affected by the change. Potential
  11.380 +INCOMPATIBILITY in rare applications of Name_Space.intern.
  11.381  
  11.382  * Basic combinators map, fold, fold_map, split_list, apply are available
  11.383  as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
  11.384 @@ -392,8 +401,8 @@
  11.385  INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
  11.386  nested.
  11.387  
  11.388 -* Synchronized.value (ML) is actually synchronized (as in Scala):
  11.389 -subtle change of semantics with minimal potential for INCOMPATIBILITY.
  11.390 +* Synchronized.value (ML) is actually synchronized (as in Scala): subtle
  11.391 +change of semantics with minimal potential for INCOMPATIBILITY.
  11.392  
  11.393  * The main operations to certify logical entities are Thm.ctyp_of and
  11.394  Thm.cterm_of with a local context; old-style global theory variants are
  11.395 @@ -404,14 +413,6 @@
  11.396  INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
  11.397  Thm.term_of etc.
  11.398  
  11.399 -* Subtle change of name space policy: undeclared entries are now
  11.400 -considered inaccessible, instead of accessible via the fully-qualified
  11.401 -internal name. This mainly affects Name_Space.intern (and derivatives),
  11.402 -which may produce an unexpected Long_Name.hidden prefix. Note that
  11.403 -contempory applications use the strict Name_Space.check (and
  11.404 -derivatives) instead, which is not affected by the change. Potential
  11.405 -INCOMPATIBILITY in rare applications of Name_Space.intern.
  11.406 -
  11.407  * Proper context for various elementary tactics: assume_tac,
  11.408  resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,
  11.409  compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.
  11.410 @@ -426,6 +427,9 @@
  11.411  @{command_keyword COMMAND} (usually without quotes and with PIDE
  11.412  markup). Minor INCOMPATIBILITY.
  11.413  
  11.414 +* Cartouches within ML sources are turned into values of type
  11.415 +Input.source (with formal position information).
  11.416 +
  11.417  
  11.418  *** System ***
  11.419  
  11.420 @@ -452,7 +456,7 @@
  11.421  semicolons from theory sources.
  11.422  
  11.423  * Support for Proof General and Isar TTY loop has been discontinued.
  11.424 -Minor INCOMPATIBILITY.
  11.425 +Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
  11.426  
  11.427  
  11.428  
    12.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Apr 11 11:56:40 2015 +0100
    12.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat Apr 11 16:19:14 2015 +0100
    12.3 @@ -565,7 +565,7 @@
    12.4    that method @{text m\<^sub>1} is applied with restriction to the first subgoal,
    12.5    then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal
    12.6    that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic
    12.7 -  combinator @{ML THEN_ALL_NEW} in Isabelle/ML, see also @{cite
    12.8 +  combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite
    12.9    "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies
   12.10    rule @{text "r"} and then solves all new subgoals by @{text blast}.
   12.11  
    13.1 --- a/src/HOL/Library/DAList_Multiset.thy	Sat Apr 11 11:56:40 2015 +0100
    13.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Sat Apr 11 16:19:14 2015 +0100
    13.3 @@ -24,7 +24,7 @@
    13.4  
    13.5  lemma [code, code del]: "image_mset = image_mset" ..
    13.6  
    13.7 -lemma [code, code del]: "Multiset.filter = Multiset.filter" ..
    13.8 +lemma [code, code del]: "filter_mset = filter_mset" ..
    13.9  
   13.10  lemma [code, code del]: "count = count" ..
   13.11  
   13.12 @@ -199,7 +199,7 @@
   13.13      (simp add: count_of_subtract_entries_raw alist.Alist_inverse
   13.14        distinct_subtract_entries_raw subtract_entries_def)
   13.15  
   13.16 -lemma filter_Bag [code]: "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
   13.17 +lemma filter_Bag [code]: "filter_mset P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
   13.18    by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
   13.19  
   13.20  
   13.21 @@ -285,7 +285,7 @@
   13.22  
   13.23  lemma DAList_Multiset_fold:
   13.24    assumes fn: "\<And>a n x. fn a n x = (f a ^^ n) x"
   13.25 -  shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al"
   13.26 +  shows "fold_mset f e (Bag al) = DAList_Multiset.fold fn e al"
   13.27    unfolding DAList_Multiset.fold_def
   13.28  proof (induct al)
   13.29    fix ys
   13.30 @@ -294,12 +294,12 @@
   13.31    have count[simp]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
   13.32      by (rule Abs_multiset_inverse[OF count_of_multiset])
   13.33    assume ys: "ys \<in> ?inv"
   13.34 -  then show "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
   13.35 +  then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
   13.36      unfolding Bag_def unfolding Alist_inverse[OF ys]
   13.37    proof (induct ys arbitrary: e rule: list.induct)
   13.38      case Nil
   13.39      show ?case
   13.40 -      by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]])
   13.41 +      by (rule trans[OF arg_cong[of _ "{#}" "fold_mset f e", OF multiset_eqI]])
   13.42           (auto, simp add: cs)
   13.43    next
   13.44      case (Cons pair ys e)
   13.45 @@ -388,7 +388,7 @@
   13.46    apply (auto simp: ac_simps)
   13.47    done
   13.48  
   13.49 -lemma size_fold: "size A = Multiset.fold (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
   13.50 +lemma size_fold: "size A = fold_mset (\<lambda>_. Suc) 0 A" (is "_ = fold_mset ?f _ _")
   13.51  proof -
   13.52    interpret comp_fun_commute ?f by default auto
   13.53    show ?thesis by (induct A) auto
   13.54 @@ -403,7 +403,7 @@
   13.55  qed
   13.56  
   13.57  
   13.58 -lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _")
   13.59 +lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
   13.60  proof -
   13.61    interpret comp_fun_commute ?f by default auto
   13.62    show ?thesis by (induct A) auto
    14.1 --- a/src/HOL/Library/Multiset.thy	Sat Apr 11 11:56:40 2015 +0100
    14.2 +++ b/src/HOL/Library/Multiset.thy	Sat Apr 11 16:19:14 2015 +0100
    14.3 @@ -527,40 +527,39 @@
    14.4  
    14.5  text {* Multiset comprehension *}
    14.6  
    14.7 -lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
    14.8 +lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
    14.9 +is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
   14.10  by (rule filter_preserves_multiset)
   14.11  
   14.12 -hide_const (open) filter
   14.13 -
   14.14 -lemma count_filter [simp]:
   14.15 -  "count (Multiset.filter P M) a = (if P a then count M a else 0)"
   14.16 -  by (simp add: filter.rep_eq)
   14.17 -
   14.18 -lemma filter_empty [simp]:
   14.19 -  "Multiset.filter P {#} = {#}"
   14.20 +lemma count_filter_mset [simp]:
   14.21 +  "count (filter_mset P M) a = (if P a then count M a else 0)"
   14.22 +  by (simp add: filter_mset.rep_eq)
   14.23 +
   14.24 +lemma filter_empty_mset [simp]:
   14.25 +  "filter_mset P {#} = {#}"
   14.26 +  by (rule multiset_eqI) simp
   14.27 +
   14.28 +lemma filter_single_mset [simp]:
   14.29 +  "filter_mset P {#x#} = (if P x then {#x#} else {#})"
   14.30    by (rule multiset_eqI) simp
   14.31  
   14.32 -lemma filter_single [simp]:
   14.33 -  "Multiset.filter P {#x#} = (if P x then {#x#} else {#})"
   14.34 +lemma filter_union_mset [simp]:
   14.35 +  "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
   14.36    by (rule multiset_eqI) simp
   14.37  
   14.38 -lemma filter_union [simp]:
   14.39 -  "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N"
   14.40 +lemma filter_diff_mset [simp]:
   14.41 +  "filter_mset P (M - N) = filter_mset P M - filter_mset P N"
   14.42    by (rule multiset_eqI) simp
   14.43  
   14.44 -lemma filter_diff [simp]:
   14.45 -  "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N"
   14.46 +lemma filter_inter_mset [simp]:
   14.47 +  "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
   14.48    by (rule multiset_eqI) simp
   14.49  
   14.50 -lemma filter_inter [simp]:
   14.51 -  "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
   14.52 -  by (rule multiset_eqI) simp
   14.53 -
   14.54 -lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
   14.55 +lemma multiset_filter_subset[simp]: "filter_mset f M \<le> M"
   14.56    unfolding less_eq_multiset.rep_eq by auto
   14.57  
   14.58  lemma multiset_filter_mono: assumes "A \<le> B"
   14.59 -  shows "Multiset.filter f A \<le> Multiset.filter f B"
   14.60 +  shows "filter_mset f A \<le> filter_mset f B"
   14.61  proof -
   14.62    from assms[unfolded mset_le_exists_conv]
   14.63    obtain C where B: "B = A + C" by auto
   14.64 @@ -572,7 +571,7 @@
   14.65  syntax (xsymbol)
   14.66    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
   14.67  translations
   14.68 -  "{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M"
   14.69 +  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
   14.70  
   14.71  
   14.72  subsubsection {* Set of elements *}
   14.73 @@ -694,7 +693,7 @@
   14.74    show ?thesis unfolding B by (induct C, auto)
   14.75  qed
   14.76  
   14.77 -lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M"
   14.78 +lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
   14.79  by (rule size_mset_mono[OF multiset_filter_subset])
   14.80  
   14.81  lemma size_Diff_submset:
   14.82 @@ -798,19 +797,19 @@
   14.83  
   14.84  subsection {* The fold combinator *}
   14.85  
   14.86 -definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
   14.87 +definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
   14.88  where
   14.89 -  "fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
   14.90 +  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
   14.91  
   14.92  lemma fold_mset_empty [simp]:
   14.93 -  "fold f s {#} = s"
   14.94 -  by (simp add: fold_def)
   14.95 +  "fold_mset f s {#} = s"
   14.96 +  by (simp add: fold_mset_def)
   14.97  
   14.98  context comp_fun_commute
   14.99  begin
  14.100  
  14.101  lemma fold_mset_insert:
  14.102 -  "fold f s (M + {#x#}) = f x (fold f s M)"
  14.103 +  "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)"
  14.104  proof -
  14.105    interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
  14.106      by (fact comp_fun_commute_funpow)
  14.107 @@ -824,7 +823,7 @@
  14.108        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
  14.109        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
  14.110      with False * show ?thesis
  14.111 -      by (simp add: fold_def del: count_union)
  14.112 +      by (simp add: fold_mset_def del: count_union)
  14.113    next
  14.114      case True
  14.115      def N \<equiv> "set_of M - {x}"
  14.116 @@ -832,23 +831,23 @@
  14.117      then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
  14.118        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
  14.119        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
  14.120 -    with * show ?thesis by (simp add: fold_def del: count_union) simp
  14.121 +    with * show ?thesis by (simp add: fold_mset_def del: count_union) simp
  14.122    qed
  14.123  qed
  14.124  
  14.125  corollary fold_mset_single [simp]:
  14.126 -  "fold f s {#x#} = f x s"
  14.127 +  "fold_mset f s {#x#} = f x s"
  14.128  proof -
  14.129 -  have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
  14.130 +  have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
  14.131    then show ?thesis by simp
  14.132  qed
  14.133  
  14.134  lemma fold_mset_fun_left_comm:
  14.135 -  "f x (fold f s M) = fold f (f x s) M"
  14.136 +  "f x (fold_mset f s M) = fold_mset f (f x s) M"
  14.137    by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
  14.138  
  14.139  lemma fold_mset_union [simp]:
  14.140 -  "fold f s (M + N) = fold f (fold f s M) N"
  14.141 +  "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
  14.142  proof (induct M)
  14.143    case empty then show ?case by simp
  14.144  next
  14.145 @@ -860,7 +859,7 @@
  14.146  
  14.147  lemma fold_mset_fusion:
  14.148    assumes "comp_fun_commute g"
  14.149 -  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P")
  14.150 +  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
  14.151  proof -
  14.152    interpret comp_fun_commute g by (fact assms)
  14.153    show "PROP ?P" by (induct A) auto
  14.154 @@ -870,10 +869,10 @@
  14.155  
  14.156  text {*
  14.157    A note on code generation: When defining some function containing a
  14.158 -  subterm @{term "fold F"}, code generation is not automatic. When
  14.159 +  subterm @{term "fold_mset F"}, code generation is not automatic. When
  14.160    interpreting locale @{text left_commutative} with @{text F}, the
  14.161 -  would be code thms for @{const fold} become thms like
  14.162 -  @{term "fold F z {#} = z"} where @{text F} is not a pattern but
  14.163 +  would be code thms for @{const fold_mset} become thms like
  14.164 +  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
  14.165    contains defined symbols, i.e.\ is not a code thm. Hence a separate
  14.166    constant with its own code thms needs to be introduced for @{text
  14.167    F}. See the image operator below.
  14.168 @@ -883,7 +882,7 @@
  14.169  subsection {* Image *}
  14.170  
  14.171  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
  14.172 -  "image_mset f = fold (plus o single o f) {#}"
  14.173 +  "image_mset f = fold_mset (plus o single o f) {#}"
  14.174  
  14.175  lemma comp_fun_commute_mset_image:
  14.176    "comp_fun_commute (plus o single o f)"
  14.177 @@ -1164,7 +1163,7 @@
  14.178  
  14.179  definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list"
  14.180  where
  14.181 -  "sorted_list_of_multiset M = fold insort [] M"
  14.182 +  "sorted_list_of_multiset M = fold_mset insort [] M"
  14.183  
  14.184  lemma sorted_list_of_multiset_empty [simp]:
  14.185    "sorted_list_of_multiset {#} = []"
  14.186 @@ -1223,7 +1222,7 @@
  14.187  
  14.188  definition F :: "'a multiset \<Rightarrow> 'a"
  14.189  where
  14.190 -  eq_fold: "F M = Multiset.fold f 1 M"
  14.191 +  eq_fold: "F M = fold_mset f 1 M"
  14.192  
  14.193  lemma empty [simp]:
  14.194    "F {#} = 1"
  14.195 @@ -1252,7 +1251,7 @@
  14.196  
  14.197  declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
  14.198  
  14.199 -lemma in_mset_fold_plus_iff[iff]: "x \<in># Multiset.fold (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
  14.200 +lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
  14.201    by (induct NN) auto
  14.202  
  14.203  notation times (infixl "*" 70)
  14.204 @@ -1353,7 +1352,7 @@
  14.205  
  14.206  lemma msetprod_multiplicity:
  14.207    "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
  14.208 -  by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
  14.209 +  by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
  14.210  
  14.211  end
  14.212  
  14.213 @@ -2101,8 +2100,6 @@
  14.214      multiset_postproc
  14.215  *}
  14.216  
  14.217 -hide_const (open) fold
  14.218 -
  14.219  
  14.220  subsection {* Naive implementation using lists *}
  14.221  
  14.222 @@ -2125,7 +2122,7 @@
  14.223    by (simp add: multiset_of_map)
  14.224  
  14.225  lemma [code]:
  14.226 -  "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)"
  14.227 +  "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
  14.228    by (simp add: multiset_of_filter)
  14.229  
  14.230  lemma [code]:
  14.231 @@ -2438,8 +2435,7 @@
  14.232      unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
  14.233      apply (rule ext)+
  14.234      apply auto
  14.235 -     apply (rule_tac x = "multiset_of (zip xs ys)" in exI)
  14.236 -     apply auto[1]
  14.237 +     apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
  14.238          apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
  14.239         apply (auto simp: list_all2_iff)[1]
  14.240        apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
  14.241 @@ -2451,7 +2447,8 @@
  14.242      apply (rule_tac x = "map fst xys" in exI)
  14.243      apply (auto simp: multiset_of_map)
  14.244      apply (rule_tac x = "map snd xys" in exI)
  14.245 -    by (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
  14.246 +    apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
  14.247 +    done
  14.248  next
  14.249    show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
  14.250      by auto
    15.1 --- a/src/HOL/Library/Sublist.thy	Sat Apr 11 11:56:40 2015 +0100
    15.2 +++ b/src/HOL/Library/Sublist.thy	Sat Apr 11 16:19:14 2015 +0100
    15.3 @@ -144,7 +144,7 @@
    15.4  
    15.5  lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
    15.6    apply (induct n arbitrary: xs ys)
    15.7 -   apply (case_tac ys, simp_all)[1]
    15.8 +   apply (case_tac ys; simp)
    15.9    apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   15.10    done
   15.11  
    16.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 11 11:56:40 2015 +0100
    16.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 11 16:19:14 2015 +0100
    16.3 @@ -190,7 +190,7 @@
    16.4          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
    16.5        in
    16.6          thy' |>
    16.7 -        BNF_LFP_Compat.add_primrec_global
    16.8 +        BNF_LFP_Compat.primrec_global
    16.9            [(Binding.name swap_name, SOME swapT, NoSyn)]
   16.10            [(Attrib.empty_binding, def1)] ||>
   16.11          Sign.parent_path ||>>
   16.12 @@ -224,7 +224,7 @@
   16.13                      Const (swap_name, swapT) $ x $ (prm $ xs $ a)));
   16.14        in
   16.15          thy' |>
   16.16 -        BNF_LFP_Compat.add_primrec_global
   16.17 +        BNF_LFP_Compat.primrec_global
   16.18            [(Binding.name prm_name, SOME prmT, NoSyn)]
   16.19            [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
   16.20          Sign.parent_path
    17.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 11 11:56:40 2015 +0100
    17.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 11 16:19:14 2015 +0100
    17.3 @@ -162,7 +162,7 @@
    17.4  fun fresh_star_const T U =
    17.5    Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
    17.6  
    17.7 -fun gen_nominal_datatype prep_specs config dts thy =
    17.8 +fun gen_nominal_datatype prep_specs (config: Old_Datatype_Aux.config) dts thy =
    17.9    let
   17.10      val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;
   17.11  
   17.12 @@ -256,7 +256,7 @@
   17.13        end) descr;
   17.14  
   17.15      val (perm_simps, thy2) =
   17.16 -      BNF_LFP_Compat.add_primrec_overloaded
   17.17 +      BNF_LFP_Compat.primrec_overloaded
   17.18          (map (fn (s, sT) => (s, sT, false))
   17.19             (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
   17.20          (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
    18.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Apr 11 11:56:40 2015 +0100
    18.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Apr 11 16:19:14 2015 +0100
    18.3 @@ -8,11 +8,11 @@
    18.4  
    18.5  signature NOMINAL_PRIMREC =
    18.6  sig
    18.7 -  val add_primrec: term list option -> term option ->
    18.8 +  val primrec: term list option -> term option ->
    18.9      (binding * typ option * mixfix) list ->
   18.10      (binding * typ option * mixfix) list ->
   18.11      (Attrib.binding * term) list -> local_theory -> Proof.state
   18.12 -  val add_primrec_cmd: string list option -> string option ->
   18.13 +  val primrec_cmd: string list option -> string option ->
   18.14      (binding * string option * mixfix) list ->
   18.15      (binding * string option * mixfix) list ->
   18.16      (Attrib.binding * string) list -> local_theory -> Proof.state
   18.17 @@ -382,8 +382,8 @@
   18.18  
   18.19  in
   18.20  
   18.21 -val add_primrec = gen_primrec Specification.check_spec (K I);
   18.22 -val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
   18.23 +val primrec = gen_primrec Specification.check_spec (K I);
   18.24 +val primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
   18.25  
   18.26  end;
   18.27  
   18.28 @@ -407,7 +407,7 @@
   18.29      "define primitive recursive functions on nominal datatypes"
   18.30      (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
   18.31        >> (fn ((((invs, fctxt), fixes), params), specs) =>
   18.32 -        add_primrec_cmd invs fctxt fixes params specs));
   18.33 +        primrec_cmd invs fctxt fixes params specs));
   18.34  
   18.35  end;
   18.36  
    19.1 --- a/src/HOL/Num.thy	Sat Apr 11 11:56:40 2015 +0100
    19.2 +++ b/src/HOL/Num.thy	Sat Apr 11 16:19:14 2015 +0100
    19.3 @@ -1195,10 +1195,10 @@
    19.4  
    19.5  declaration {*
    19.6  let 
    19.7 -  fun number_of thy T n =
    19.8 -    if not (Sign.of_sort thy (T, @{sort numeral}))
    19.9 +  fun number_of ctxt T n =
   19.10 +    if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
   19.11      then raise CTERM ("number_of", [])
   19.12 -    else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n;
   19.13 +    else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
   19.14  in
   19.15    K (
   19.16      Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}
    20.1 --- a/src/HOL/Probability/measurable.ML	Sat Apr 11 11:56:40 2015 +0100
    20.2 +++ b/src/HOL/Probability/measurable.ML	Sat Apr 11 16:19:14 2015 +0100
    20.3 @@ -51,14 +51,14 @@
    20.4      dest_thms : thm Item_Net.T,
    20.5      cong_thms : thm Item_Net.T,
    20.6      preprocessors : (string * preprocessor) list }
    20.7 -  val empty = {
    20.8 +  val empty: T = {
    20.9      measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
   20.10      dest_thms = Thm.full_rules,
   20.11      cong_thms = Thm.full_rules,
   20.12      preprocessors = [] };
   20.13    val extend = I;
   20.14    fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
   20.15 -      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) = {
   20.16 +      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
   20.17      measurable_thms = Item_Net.merge (t1, t2),
   20.18      dest_thms = Item_Net.merge (dt1, dt2),
   20.19      cong_thms = Item_Net.merge (ct1, ct2),
   20.20 @@ -81,7 +81,7 @@
   20.21  fun map_cong_thms f = map_data I I f I
   20.22  fun map_preprocessors f = map_data I I I f
   20.23  
   20.24 -fun generic_add_del map = 
   20.25 +fun generic_add_del map : attribute context_parser =
   20.26    Scan.lift
   20.27      (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
   20.28      (fn f => Thm.declaration_attribute (Data.map o map o f))
    21.1 --- a/src/HOL/ROOT	Sat Apr 11 11:56:40 2015 +0100
    21.2 +++ b/src/HOL/ROOT	Sat Apr 11 16:19:14 2015 +0100
    21.3 @@ -229,7 +229,7 @@
    21.4    document_files "root.bib" "root.tex"
    21.5  
    21.6  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
    21.7 -  options [document = false, browser_info = false]
    21.8 +  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
    21.9    theories
   21.10      Generate
   21.11      Generate_Binary_Nat
   21.12 @@ -673,7 +673,7 @@
   21.13  
   21.14      TPTP-related extensions.
   21.15    *}
   21.16 -  options [document = false]
   21.17 +  options [condition = ML_SYSTEM_POLYML, document = false]
   21.18    theories
   21.19      ATP_Theory_Export
   21.20      MaSh_Eval
   21.21 @@ -806,7 +806,7 @@
   21.22    theories Mirabelle_Test
   21.23  
   21.24  session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   21.25 -  options [document = false, timeout = 60]
   21.26 +  options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
   21.27    theories Ex
   21.28  
   21.29  session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
    22.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Apr 11 11:56:40 2015 +0100
    22.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Apr 11 16:19:14 2015 +0100
    22.3 @@ -8,7 +8,7 @@
    22.4  
    22.5  signature BNF_COMP =
    22.6  sig
    22.7 -  val inline_threshold: int Config.T
    22.8 +  val typedef_threshold: int Config.T
    22.9  
   22.10    val ID_bnf: BNF_Def.bnf
   22.11    val DEADID_bnf: BNF_Def.bnf
   22.12 @@ -76,7 +76,7 @@
   22.13  open BNF_Tactics
   22.14  open BNF_Comp_Tactics
   22.15  
   22.16 -val inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
   22.17 +val typedef_threshold = Attrib.setup_config_int @{binding bnf_typedef_threshold} (K 6);
   22.18  
   22.19  val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
   22.20  val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
   22.21 @@ -755,10 +755,10 @@
   22.22  
   22.23  fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
   22.24    let
   22.25 -    val threshold = Config.get ctxt inline_threshold;
   22.26 +    val threshold = Config.get ctxt typedef_threshold;
   22.27      val repT = HOLogic.dest_setT (fastype_of set);
   22.28      val out_of_line = force_out_of_line orelse
   22.29 -      (threshold >= 0 andalso Term.size_of_typ repT > threshold);
   22.30 +      (threshold >= 0 andalso Term.size_of_typ repT >= threshold);
   22.31    in
   22.32      if out_of_line then
   22.33        typedef (b, As, mx) set opt_morphs tac
    23.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Apr 11 11:56:40 2015 +0100
    23.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Apr 11 16:19:14 2015 +0100
    23.3 @@ -49,7 +49,7 @@
    23.4    val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
    23.5      term -> 'a -> 'a
    23.6    val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
    23.7 -    typ list -> term -> term
    23.8 +    (typ list -> term -> unit) -> typ list -> term -> term
    23.9    val massage_nested_corec_call: Proof.context -> (term -> bool) ->
   23.10      (typ list -> typ -> typ -> term -> term) -> (typ list -> typ -> typ -> term -> term) ->
   23.11      typ list -> typ -> typ -> term -> term
   23.12 @@ -70,10 +70,10 @@
   23.13    val gfp_rec_sugar_interpretation: string ->
   23.14      (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
   23.15  
   23.16 -  val add_primcorecursive_cmd: corec_option list ->
   23.17 +  val primcorecursive_cmd: corec_option list ->
   23.18      (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
   23.19      Proof.context -> Proof.state
   23.20 -  val add_primcorec_cmd: corec_option list ->
   23.21 +  val primcorec_cmd: corec_option list ->
   23.22      (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
   23.23      local_theory -> local_theory
   23.24  end;
   23.25 @@ -243,11 +243,11 @@
   23.26      SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
   23.27    | _ => NONE);
   23.28  
   23.29 -fun massage_let_if_case ctxt has_call massage_leaf bound_Ts t0 =
   23.30 +fun massage_let_if_case ctxt has_call massage_leaf unexpected_call bound_Ts t0 =
   23.31    let
   23.32      val thy = Proof_Context.theory_of ctxt;
   23.33  
   23.34 -    fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else ();
   23.35 +    fun check_no_call bound_Ts t = if has_call t then unexpected_call bound_Ts t else ();
   23.36  
   23.37      fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t
   23.38        | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t)
   23.39 @@ -264,7 +264,8 @@
   23.40              (dummy_branch' :: _, []) => dummy_branch'
   23.41            | (_, [branch']) => branch'
   23.42            | (_, branches') =>
   23.43 -            Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches'))
   23.44 +            Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
   23.45 +              branches'))
   23.46          | (c as Const (@{const_name case_prod}, _), arg :: args) =>
   23.47            massage_rec bound_Ts
   23.48              (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
   23.49 @@ -287,7 +288,7 @@
   23.50                        val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
   23.51                      in
   23.52                        Term.list_comb (casex',
   23.53 -                        branches' @ tap (List.app check_no_call) obj_leftovers)
   23.54 +                        branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers)
   23.55                      end
   23.56                    else
   23.57                      massage_leaf bound_Ts t
   23.58 @@ -304,6 +305,9 @@
   23.59        if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t)
   23.60    end;
   23.61  
   23.62 +fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 =
   23.63 +  massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0])) bound_Ts t0;
   23.64 +
   23.65  fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
   23.66  
   23.67  fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 =
   23.68 @@ -348,7 +352,7 @@
   23.69              (betapply (t, var))))
   23.70          end)
   23.71      and massage_any_call bound_Ts U T =
   23.72 -      massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
   23.73 +      massage_let_if_case_corec ctxt has_call (fn bound_Ts => fn t =>
   23.74          if has_call t then
   23.75            (case U of
   23.76              Type (s, Us) =>
   23.77 @@ -384,8 +388,6 @@
   23.78            | _ => ill_formed_corec_call ctxt t)
   23.79          else
   23.80            massage_noncall bound_Ts U T t) bound_Ts;
   23.81 -
   23.82 -    val T = fastype_of1 (bound_Ts, t0);
   23.83    in
   23.84      (if has_call t0 then massage_any_call else massage_noncall) bound_Ts U T t0
   23.85    end;
   23.86 @@ -399,12 +401,12 @@
   23.87  fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   23.88    (case fastype_of1 (bound_Ts, t) of
   23.89      Type (s, Ts) =>
   23.90 -    massage_let_if_case ctxt has_call (fn _ => fn t =>
   23.91 +    massage_let_if_case_corec ctxt has_call (fn _ => fn t =>
   23.92        if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t
   23.93    | _ => raise Fail "expand_corec_code_rhs");
   23.94  
   23.95  fun massage_corec_code_rhs ctxt massage_ctr =
   23.96 -  massage_let_if_case ctxt (K false)
   23.97 +  massage_let_if_case_corec ctxt (K false)
   23.98      (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
   23.99  
  23.100  fun fold_rev_corec_code_rhs ctxt f =
  23.101 @@ -883,7 +885,7 @@
  23.102        fun rewrite_end _ t = if has_call t then undef_const else t;
  23.103        fun rewrite_cont bound_Ts t =
  23.104          if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
  23.105 -      fun massage f _ = massage_let_if_case ctxt has_call f bound_Ts rhs_term
  23.106 +      fun massage f _ = massage_let_if_case_corec ctxt has_call f bound_Ts rhs_term
  23.107          |> abs_tuple_balanced fun_args;
  23.108      in
  23.109        (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
  23.110 @@ -1039,7 +1041,7 @@
  23.111  fun is_trivial_implies thm =
  23.112    uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
  23.113  
  23.114 -fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy =
  23.115 +fun primcorec_ursive auto opts fixes specs of_specs_opt lthy =
  23.116    let
  23.117      val thy = Proof_Context.theory_of lthy;
  23.118  
  23.119 @@ -1525,7 +1527,7 @@
  23.120      (goalss, after_qed, lthy')
  23.121    end;
  23.122  
  23.123 -fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
  23.124 +fun primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
  23.125    let
  23.126      val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
  23.127      val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
  23.128 @@ -1534,18 +1536,18 @@
  23.129        split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
  23.130      val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
  23.131    in
  23.132 -    add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
  23.133 +    primcorec_ursive auto opts fixes specs of_specs_opt lthy
  23.134    end;
  23.135  
  23.136 -val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
  23.137 +val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
  23.138    lthy
  23.139    |> Proof.theorem NONE after_qed goalss
  23.140    |> Proof.refine (Method.primitive_text (K I))
  23.141 -  |> Seq.hd) ooo add_primcorec_ursive_cmd false;
  23.142 +  |> Seq.hd) ooo primcorec_ursive_cmd false;
  23.143  
  23.144 -val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
  23.145 +val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
  23.146      lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
  23.147 -  add_primcorec_ursive_cmd true;
  23.148 +  primcorec_ursive_cmd true;
  23.149  
  23.150  val corec_option_parser = Parse.group (K "option")
  23.151    (Plugin_Name.parse_filter >> Plugins_Option
  23.152 @@ -1560,13 +1562,13 @@
  23.153    "define primitive corecursive functions"
  23.154    ((Scan.optional (@{keyword "("} |--
  23.155        Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
  23.156 -    (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
  23.157 +    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
  23.158  
  23.159  val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
  23.160    "define primitive corecursive functions"
  23.161    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
  23.162        --| @{keyword ")"}) []) --
  23.163 -    (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorec_cmd);
  23.164 +    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
  23.165  
  23.166  val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
  23.167    gfp_rec_sugar_transfer_interpretation);
    24.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sat Apr 11 11:56:40 2015 +0100
    24.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sat Apr 11 16:19:14 2015 +0100
    24.3 @@ -26,14 +26,14 @@
    24.4    val datatype_compat_global: string list -> theory -> theory
    24.5    val datatype_compat_cmd: string list -> local_theory -> local_theory
    24.6    val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
    24.7 -  val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    24.8 +  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    24.9      local_theory -> (term list * thm list) * local_theory
   24.10 -  val add_primrec_global: (binding * typ option * mixfix) list ->
   24.11 +  val primrec_global: (binding * typ option * mixfix) list ->
   24.12      (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   24.13 -  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   24.14 +  val primrec_overloaded: (string * (string * typ) * bool) list ->
   24.15      (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
   24.16      (term list * thm list) * theory
   24.17 -  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   24.18 +  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   24.19      local_theory -> (string list * (term list * thm list)) * local_theory
   24.20  end;
   24.21  
   24.22 @@ -532,11 +532,12 @@
   24.23       |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
   24.24    end;
   24.25  
   24.26 -val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
   24.27 -val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
   24.28 -val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
   24.29 -val add_primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo
   24.30 -  BNF_LFP_Rec_Sugar.add_primrec_simple;
   24.31 +fun old_of_new f (ts, _, simpss) = (ts, f simpss);
   24.32 +
   24.33 +val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec;
   24.34 +val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global;
   24.35 +val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded;
   24.36 +val primrec_simple = apfst (apsnd (old_of_new (flat o snd))) ooo BNF_LFP_Rec_Sugar.primrec_simple;
   24.37  
   24.38  val _ =
   24.39    Outer_Syntax.local_theory @{command_keyword datatype_compat}
    25.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Apr 11 11:56:40 2015 +0100
    25.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Apr 11 16:19:14 2015 +0100
    25.3 @@ -61,17 +61,18 @@
    25.4    val lfp_rec_sugar_interpretation: string ->
    25.5      (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
    25.6  
    25.7 -  val add_primrec: (binding * typ option * mixfix) list ->
    25.8 -    (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
    25.9 -  val add_primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
   25.10 -    (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory
   25.11 -  val add_primrec_global: (binding * typ option * mixfix) list ->
   25.12 -    (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
   25.13 -  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   25.14 +  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
   25.15 +    local_theory -> (term list * thm list * thm list list) * local_theory
   25.16 +  val primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
   25.17 +    (Attrib.binding * string) list -> local_theory ->
   25.18 +    (term list * thm list * thm list list) * local_theory
   25.19 +  val primrec_global: (binding * typ option * mixfix) list ->
   25.20 +    (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
   25.21 +  val primrec_overloaded: (string * (string * typ) * bool) list ->
   25.22      (binding * typ option * mixfix) list ->
   25.23 -    (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
   25.24 -  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   25.25 -    local_theory -> (string list * (term list * (int list list * thm list list))) * local_theory
   25.26 +    (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
   25.27 +  val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory ->
   25.28 +    (string list * (term list * thm list * (int list list * thm list list))) * local_theory
   25.29  end;
   25.30  
   25.31  structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR =
   25.32 @@ -546,7 +547,7 @@
   25.33            find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
   25.34              fun_data eqns_data;
   25.35  
   25.36 -        val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
   25.37 +        val simps = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
   25.38            |> fst
   25.39            |> map_filter (try (fn (x, [y]) =>
   25.40              (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
   25.41 @@ -556,7 +557,7 @@
   25.42                |> K |> Goal.prove_sorry lthy' [] [] user_eqn
   25.43                |> Thm.close_derivation);
   25.44        in
   25.45 -        ((js, simp_thms), lthy')
   25.46 +        ((js, simps), lthy')
   25.47        end;
   25.48  
   25.49      val notes =
   25.50 @@ -591,7 +592,7 @@
   25.51        lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   25.52    end;
   25.53  
   25.54 -fun add_primrec_simple0 plugins nonexhaustive transfer fixes ts lthy =
   25.55 +fun primrec_simple0 plugins nonexhaustive transfer fixes ts lthy =
   25.56    let
   25.57      val actual_nn = length fixes;
   25.58  
   25.59 @@ -604,20 +605,19 @@
   25.60      lthy'
   25.61      |> fold_map Local_Theory.define defs
   25.62      |-> (fn defs => fn lthy =>
   25.63 -      let val (thms, lthy) = prove lthy defs;
   25.64 -      in ((names, (map fst defs, thms)), lthy) end)
   25.65 +      let val ((jss, simpss), lthy) = prove lthy defs;
   25.66 +      in ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) end)
   25.67    end;
   25.68  
   25.69 -fun add_primrec_simple fixes ts lthy =
   25.70 -  add_primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
   25.71 +fun primrec_simple fixes ts lthy =
   25.72 +  primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
   25.73    handle OLD_PRIMREC () =>
   25.74 -    Old_Primrec.add_primrec_simple fixes ts lthy
   25.75 -    |>> apsnd (apsnd (pair [] o single)) o apfst single;
   25.76 +    Old_Primrec.primrec_simple fixes ts lthy
   25.77 +    |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single;
   25.78  
   25.79 -fun gen_primrec old_primrec prep_spec opts
   25.80 -    (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
   25.81 +fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy =
   25.82    let
   25.83 -    val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
   25.84 +    val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes);
   25.85      val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
   25.86  
   25.87      val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
   25.88 @@ -643,25 +643,27 @@
   25.89          end);
   25.90    in
   25.91      lthy
   25.92 -    |> add_primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
   25.93 -    |-> (fn (names, (ts, (jss, simpss))) =>
   25.94 +    |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
   25.95 +    |-> (fn (names, (ts, defs, (jss, simpss))) =>
   25.96        Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
   25.97        #> Local_Theory.notes (mk_notes jss names simpss)
   25.98 -      #>> pair ts o map snd)
   25.99 +      #>> (fn notes => (ts, defs, map snd notes)))
  25.100    end
  25.101 -  handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single;
  25.102 +  handle OLD_PRIMREC () =>
  25.103 +    old_primrec raw_fixes raw_specs lthy
  25.104 +    |>> (fn (ts, thms) => (ts, [], [thms]));
  25.105  
  25.106 -val add_primrec = gen_primrec Old_Primrec.add_primrec Specification.check_spec [];
  25.107 -val add_primrec_cmd = gen_primrec Old_Primrec.add_primrec_cmd Specification.read_spec;
  25.108 +val primrec = gen_primrec Old_Primrec.primrec Specification.check_spec [];
  25.109 +val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_spec;
  25.110  
  25.111 -fun add_primrec_global fixes specs =
  25.112 +fun primrec_global fixes specs =
  25.113    Named_Target.theory_init
  25.114 -  #> add_primrec fixes specs
  25.115 +  #> primrec fixes specs
  25.116    ##> Local_Theory.exit_global;
  25.117  
  25.118 -fun add_primrec_overloaded ops fixes specs =
  25.119 +fun primrec_overloaded ops fixes specs =
  25.120    Overloading.overloading ops
  25.121 -  #> add_primrec fixes specs
  25.122 +  #> primrec fixes specs
  25.123    ##> Local_Theory.exit_global;
  25.124  
  25.125  val rec_option_parser = Parse.group (K "option")
  25.126 @@ -674,6 +676,6 @@
  25.127    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
  25.128        --| @{keyword ")"}) []) --
  25.129      (Parse.fixes -- Parse_Spec.where_alt_specs)
  25.130 -    >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs));
  25.131 +    >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
  25.132  
  25.133  end;
    26.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Sat Apr 11 11:56:40 2015 +0100
    26.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Sat Apr 11 16:19:14 2015 +0100
    26.3 @@ -6,7 +6,13 @@
    26.4  More recursor sugar.
    26.5  *)
    26.6  
    26.7 -structure BNF_LFP_Rec_Sugar_More : sig end =
    26.8 +signature BNF_LFP_REC_SUGAR_MORE =
    26.9 +sig
   26.10 +  val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
   26.11 +    (typ * typ -> term) -> typ list -> term -> term -> term -> term
   26.12 +end;
   26.13 +
   26.14 +structure BNF_LFP_Rec_Sugar_More : BNF_LFP_REC_SUGAR_MORE =
   26.15  struct
   26.16  
   26.17  open BNF_Util
   26.18 @@ -68,20 +74,20 @@
   26.19    error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
   26.20  fun invalid_map ctxt t =
   26.21    error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
   26.22 -fun unexpected_rec_call ctxt t =
   26.23 -  error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
   26.24 +fun unexpected_rec_call ctxt eqns t =
   26.25 +  error_at ctxt eqns ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t));
   26.26  
   26.27 -fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
   26.28 +fun massage_nested_rec_call ctxt has_call massage_fun massage_nonfun bound_Ts y y' t0 =
   26.29    let
   26.30 -    fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
   26.31 +    fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else ();
   26.32  
   26.33      val typof = curry fastype_of1 bound_Ts;
   26.34 -    val build_map_fst = build_map ctxt [] (fst_const o fst);
   26.35 +    val massage_no_call = build_map ctxt [] massage_nonfun;
   26.36  
   26.37      val yT = typof y;
   26.38      val yU = typof y';
   26.39  
   26.40 -    fun y_of_y' () = build_map_fst (yU, yT) $ y';
   26.41 +    fun y_of_y' () = massage_no_call (yU, yT) $ y';
   26.42      val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
   26.43  
   26.44      fun massage_mutual_fun U T t =
   26.45 @@ -89,12 +95,7 @@
   26.46          Const (@{const_name comp}, _) $ t1 $ t2 =>
   26.47          mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2)
   26.48        | _ =>
   26.49 -        if has_call t then
   26.50 -          (case try HOLogic.dest_prodT U of
   26.51 -            SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t
   26.52 -          | NONE => invalid_map ctxt t)
   26.53 -        else
   26.54 -          mk_comp bound_Ts (t, build_map_fst (U, T)));
   26.55 +        if has_call t then massage_fun U T t else mk_comp bound_Ts (t, massage_no_call (U, T)));
   26.56  
   26.57      fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
   26.58          (case try (dest_map ctxt s) t of
   26.59 @@ -115,7 +116,7 @@
   26.60          massage_map U T t
   26.61          handle NO_MAP _ => massage_mutual_fun U T t;
   26.62  
   26.63 -    fun massage_call (t as t1 $ t2) =
   26.64 +    fun massage_outer_call (t as t1 $ t2) =
   26.65          if has_call t then
   26.66            if t2 = y then
   26.67              massage_map yU yT (elim_y t1) $ y'
   26.68 @@ -123,25 +124,28 @@
   26.69            else
   26.70              let val (g, xs) = Term.strip_comb t2 in
   26.71                if g = y then
   26.72 -                if exists has_call xs then unexpected_rec_call ctxt t2
   26.73 -                else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs)
   26.74 +                if exists has_call xs then unexpected_rec_call ctxt [t0] t2
   26.75 +                else Term.list_comb (massage_outer_call (mk_compN (length xs) bound_Ts (t1, y)), xs)
   26.76                else
   26.77                  ill_formed_rec_call ctxt t
   26.78              end
   26.79          else
   26.80            elim_y t
   26.81 -      | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
   26.82 +      | massage_outer_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
   26.83    in
   26.84 -    massage_call
   26.85 +    massage_outer_call t0
   26.86    end;
   26.87  
   26.88 -fun rewrite_map_arg ctxt get_ctr_pos rec_type res_type =
   26.89 +fun rewrite_map_fun ctxt get_ctr_pos U T t =
   26.90    let
   26.91 -    val pT = HOLogic.mk_prodT (rec_type, res_type);
   26.92 +    val _ =
   26.93 +      (case try HOLogic.dest_prodT U of
   26.94 +        SOME (U1, _) => U1 = T orelse invalid_map ctxt t
   26.95 +      | NONE => invalid_map ctxt t);
   26.96  
   26.97 -    fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT)
   26.98 +    fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const U)
   26.99        | subst d (Abs (v, T, b)) =
  26.100 -        Abs (v, if d = SOME ~1 then pT else T, subst (Option.map (Integer.add 1) d) b)
  26.101 +        Abs (v, if d = SOME ~1 then U else T, subst (Option.map (Integer.add 1) d) b)
  26.102        | subst d t =
  26.103          let
  26.104            val (u, vs) = strip_comb t;
  26.105 @@ -149,22 +153,22 @@
  26.106          in
  26.107            if ctr_pos >= 0 then
  26.108              if d = SOME ~1 andalso length vs = ctr_pos then
  26.109 -              Term.list_comb (permute_args ctr_pos (snd_const pT), vs)
  26.110 +              Term.list_comb (permute_args ctr_pos (snd_const U), vs)
  26.111              else if length vs > ctr_pos andalso is_some d andalso
  26.112                  d = try (fn Bound n => n) (nth vs ctr_pos) then
  26.113 -              Term.list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
  26.114 +              Term.list_comb (snd_const U $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
  26.115              else
  26.116                error ("Recursive call not directly applied to constructor argument in " ^
  26.117                  quote (Syntax.string_of_term ctxt t))
  26.118            else
  26.119 -            Term.list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
  26.120 -        end
  26.121 +            Term.list_comb (u, map (subst (if d = SOME ~1 then NONE else d)) vs)
  26.122 +        end;
  26.123    in
  26.124 -    subst (SOME ~1)
  26.125 +    subst (SOME ~1) t
  26.126    end;
  26.127  
  26.128  fun rewrite_nested_rec_call ctxt has_call get_ctr_pos =
  26.129 -  massage_nested_rec_call ctxt has_call (rewrite_map_arg ctxt get_ctr_pos);
  26.130 +  massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos) (fst_const o fst);
  26.131  
  26.132  val _ = Theory.setup (register_lfp_rec_extension
  26.133    {nested_simps = nested_simps, is_new_datatype = is_new_datatype,
    27.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sat Apr 11 11:56:40 2015 +0100
    27.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sat Apr 11 16:19:14 2015 +0100
    27.3 @@ -8,16 +8,16 @@
    27.4  
    27.5  signature OLD_PRIMREC =
    27.6  sig
    27.7 -  val add_primrec: (binding * typ option * mixfix) list ->
    27.8 +  val primrec: (binding * typ option * mixfix) list ->
    27.9      (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory
   27.10 -  val add_primrec_cmd: (binding * string option * mixfix) list ->
   27.11 +  val primrec_cmd: (binding * string option * mixfix) list ->
   27.12      (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory
   27.13 -  val add_primrec_global: (binding * typ option * mixfix) list ->
   27.14 +  val primrec_global: (binding * typ option * mixfix) list ->
   27.15      (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   27.16 -  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   27.17 +  val primrec_overloaded: (string * (string * typ) * bool) list ->
   27.18      (binding * typ option * mixfix) list ->
   27.19      (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   27.20 -  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   27.21 +  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   27.22      local_theory -> (string * (term list * thm list)) * local_theory
   27.23  end;
   27.24  
   27.25 @@ -260,7 +260,7 @@
   27.26  
   27.27  (* primrec definition *)
   27.28  
   27.29 -fun add_primrec_simple fixes ts lthy =
   27.30 +fun primrec_simple fixes ts lthy =
   27.31    let
   27.32      val ((prefix, (_, defs)), prove) = distill lthy fixes ts;
   27.33    in
   27.34 @@ -280,7 +280,7 @@
   27.35        (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   27.36    in
   27.37      lthy
   27.38 -    |> add_primrec_simple fixes (map snd spec)
   27.39 +    |> primrec_simple fixes (map snd spec)
   27.40      |-> (fn (prefix, (ts, simps)) =>
   27.41        Spec_Rules.add Spec_Rules.Equational (ts, simps)
   27.42        #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
   27.43 @@ -290,22 +290,22 @@
   27.44  
   27.45  in
   27.46  
   27.47 -val add_primrec = gen_primrec Specification.check_spec;
   27.48 -val add_primrec_cmd = gen_primrec Specification.read_spec;
   27.49 +val primrec = gen_primrec Specification.check_spec;
   27.50 +val primrec_cmd = gen_primrec Specification.read_spec;
   27.51  
   27.52  end;
   27.53  
   27.54 -fun add_primrec_global fixes specs thy =
   27.55 +fun primrec_global fixes specs thy =
   27.56    let
   27.57      val lthy = Named_Target.theory_init thy;
   27.58 -    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
   27.59 +    val ((ts, simps), lthy') = primrec fixes specs lthy;
   27.60      val simps' = Proof_Context.export lthy' lthy simps;
   27.61    in ((ts, simps'), Local_Theory.exit_global lthy') end;
   27.62  
   27.63 -fun add_primrec_overloaded ops fixes specs thy =
   27.64 +fun primrec_overloaded ops fixes specs thy =
   27.65    let
   27.66      val lthy = Overloading.overloading ops thy;
   27.67 -    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
   27.68 +    val ((ts, simps), lthy') = primrec fixes specs lthy;
   27.69      val simps' = Proof_Context.export lthy' lthy simps;
   27.70    in ((ts, simps'), Local_Theory.exit_global lthy') end;
   27.71  
    28.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Apr 11 11:56:40 2015 +0100
    28.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Apr 11 16:19:14 2015 +0100
    28.3 @@ -96,7 +96,7 @@
    28.4        subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
    28.5      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
    28.6      val ((_, (_, eqs2)), lthy') = lthy
    28.7 -      |> BNF_LFP_Compat.add_primrec_simple
    28.8 +      |> BNF_LFP_Compat.primrec_simple
    28.9          [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
   28.10      val cT_random_aux = inst pt_random_aux;
   28.11      val cT_rhs = inst pt_rhs;
    29.1 --- a/src/HOL/Tools/int_arith.ML	Sat Apr 11 11:56:40 2015 +0100
    29.2 +++ b/src/HOL/Tools/int_arith.ML	Sat Apr 11 16:19:14 2015 +0100
    29.3 @@ -79,10 +79,10 @@
    29.4    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    29.5    proc = sproc, identifier = []}
    29.6  
    29.7 -fun number_of thy T n =
    29.8 -  if not (Sign.of_sort thy (T, @{sort numeral}))
    29.9 +fun number_of ctxt T n =
   29.10 +  if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
   29.11    then raise CTERM ("number_of", [])
   29.12 -  else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n;
   29.13 +  else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
   29.14  
   29.15  val setup =
   29.16    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    30.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Apr 11 11:56:40 2015 +0100
    30.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Apr 11 16:19:14 2015 +0100
    30.3 @@ -16,7 +16,7 @@
    30.4    val add_simprocs: simproc list -> Context.generic -> Context.generic
    30.5    val add_inj_const: string * typ -> Context.generic -> Context.generic
    30.6    val add_discrete_type: string -> Context.generic -> Context.generic
    30.7 -  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
    30.8 +  val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
    30.9    val setup: Context.generic -> Context.generic
   30.10    val global_setup: theory -> theory
   30.11    val split_limit: int Config.T
    31.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat Apr 11 11:56:40 2015 +0100
    31.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Apr 11 16:19:14 2015 +0100
    31.3 @@ -91,16 +91,16 @@
    31.4    val map_data:
    31.5      ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    31.6        lessD: thm list, neqE: thm list, simpset: simpset,
    31.7 -      number_of: (theory -> typ -> int -> cterm) option} ->
    31.8 +      number_of: (Proof.context -> typ -> int -> cterm) option} ->
    31.9       {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   31.10        lessD: thm list, neqE: thm list, simpset: simpset,
   31.11 -      number_of: (theory -> typ -> int -> cterm) option}) ->
   31.12 +      number_of: (Proof.context -> typ -> int -> cterm) option}) ->
   31.13        Context.generic -> Context.generic
   31.14    val add_inj_thms: thm list -> Context.generic -> Context.generic
   31.15    val add_lessD: thm -> Context.generic -> Context.generic
   31.16    val add_simps: thm list -> Context.generic -> Context.generic
   31.17    val add_simprocs: simproc list -> Context.generic -> Context.generic
   31.18 -  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
   31.19 +  val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
   31.20  end;
   31.21  
   31.22  functor Fast_Lin_Arith
   31.23 @@ -119,7 +119,7 @@
   31.24      lessD: thm list,
   31.25      neqE: thm list,
   31.26      simpset: simpset,
   31.27 -    number_of: (theory -> typ -> int -> cterm) option};
   31.28 +    number_of: (Proof.context -> typ -> int -> cterm) option};
   31.29  
   31.30    val empty : T =
   31.31     {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
   31.32 @@ -169,7 +169,7 @@
   31.33  
   31.34  fun number_of ctxt =
   31.35    (case Data.get (Context.Proof ctxt) of
   31.36 -    {number_of = SOME f, ...} => f (Proof_Context.theory_of ctxt)
   31.37 +    {number_of = SOME f, ...} => f ctxt
   31.38    | _ => fn _ => fn _ => raise CTERM ("number_of", []));
   31.39  
   31.40  
    32.1 --- a/src/Pure/drule.ML	Sat Apr 11 11:56:40 2015 +0100
    32.2 +++ b/src/Pure/drule.ML	Sat Apr 11 16:19:14 2015 +0100
    32.3 @@ -204,10 +204,12 @@
    32.4      val ps = outer_params (Thm.term_of goal)
    32.5        |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
    32.6      val Ts = map Term.fastype_of ps;
    32.7 -    val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) =>
    32.8 -      (Thm.global_cterm_of thy (Var (xi, T)), Thm.global_cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps))));
    32.9 +    val inst =
   32.10 +      Thm.fold_terms Term.add_vars th []
   32.11 +      |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
   32.12    in
   32.13 -    th |> Thm.instantiate ([], inst)
   32.14 +    th
   32.15 +    |> Thm.instantiate (Thm.certify_inst thy ([], inst))
   32.16      |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
   32.17    end;
   32.18  
   32.19 @@ -228,12 +230,10 @@
   32.20    | zero_var_indexes_list ths =
   32.21        let
   32.22          val thy = Theory.merge_list (map Thm.theory_of_thm ths);
   32.23 -        val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
   32.24 -        val cinstT =
   32.25 -          map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT;
   32.26 -        val cinst =
   32.27 -          map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst;
   32.28 -      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
   32.29 +        val inst =
   32.30 +          Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
   32.31 +          |> Thm.certify_inst thy;
   32.32 +      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
   32.33  
   32.34  val zero_var_indexes = singleton zero_var_indexes_list;
   32.35  
   32.36 @@ -629,9 +629,9 @@
   32.37    let
   32.38      val thy = Thm.theory_of_cterm ct;
   32.39      val T = Thm.typ_of_cterm ct;
   32.40 -    val a = Thm.global_ctyp_of thy (TVar (("'a", 0), []));
   32.41 +    val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T);
   32.42      val x = Thm.global_cterm_of thy (Var (("x", 0), T));
   32.43 -  in Thm.instantiate ([(a, Thm.global_ctyp_of thy T)], [(x, ct)]) termI end;
   32.44 +  in Thm.instantiate ([instT], [(x, ct)]) termI end;
   32.45  
   32.46  fun dest_term th =
   32.47    let val cprop = strip_imp_concl (Thm.cprop_of th) in
    33.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Apr 11 11:56:40 2015 +0100
    33.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Apr 11 16:19:14 2015 +0100
    33.3 @@ -8,8 +8,8 @@
    33.4  
    33.5  signature PRIMREC_PACKAGE =
    33.6  sig
    33.7 -  val add_primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
    33.8 -  val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
    33.9 +  val primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
   33.10 +  val primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
   33.11  end;
   33.12  
   33.13  structure PrimrecPackage : PRIMREC_PACKAGE =
   33.14 @@ -161,7 +161,7 @@
   33.15  
   33.16  (* prepare functions needed for definitions *)
   33.17  
   33.18 -fun add_primrec_i args thy =
   33.19 +fun primrec_i args thy =
   33.20    let
   33.21      val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
   33.22      val SOME (fname, ftype, ls, rs, con_info, eqns) =
   33.23 @@ -188,8 +188,8 @@
   33.24        ||> Sign.parent_path;
   33.25    in (thy3, eqn_thms') end;
   33.26  
   33.27 -fun add_primrec args thy =
   33.28 -  add_primrec_i (map (fn ((name, s), srcs) =>
   33.29 +fun primrec args thy =
   33.30 +  primrec_i (map (fn ((name, s), srcs) =>
   33.31      ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs))
   33.32      args) thy;
   33.33  
   33.34 @@ -199,7 +199,7 @@
   33.35  val _ =
   33.36    Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
   33.37      (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
   33.38 -      >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
   33.39 +      >> (Toplevel.theory o (#1 oo (primrec o map Parse.triple_swap))));
   33.40  
   33.41  end;
   33.42