Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Datatype/primrec.ML
changeset 56245 84fc7dfa3cd4
parent 55575 a5e33e18fb5c 
--- a/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Datatype/primrec.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -34,8 +34,8 @@
 
 fun process_eqn is_fixed spec rec_fns =
   let
-    val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
-    val body = strip_qnt_body "all" spec;
+    val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} spec);
+    val body = strip_qnt_body @{const_name Pure.all} spec;
     val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
       (fn Free (v, _) => insert (op =) v | _ => I) body []));
     val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
isabelle