# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1400494788 -3600
# Node ID 08c3ef07cef78e3ae595b4d2ec698f7751330543
# Parent  9ae285ce814ef836ac63078d4ed09eb87c5f4c8d
changes from upstream

diff -r 9ae285ce814e -r 08c3ef07cef7 Nominal/Atoms.thy
--- a/Nominal/Atoms.thy	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/Atoms.thy	Mon May 19 11:19:48 2014 +0100
@@ -71,34 +71,6 @@
 
 term "a:::name"
 
-text {* 
-  a:::name stands for (atom a) with a being of concrete atom 
-  type name. The above lemma can therefore also be stated as
-
-  "sort_of (a:::name) = Sort ''name'' []"
-
-  This does not work for multi-sorted atoms.
-*}
-
-(* fixme 
-lemma supp_of_finite_name_set:
-  fixes S::"name set"
-  assumes "infinte S" "infinite (UNIV - S)"
-  shows "supp S = UNIV"
-proof -
-  { fix a    
-    have "a \<in> supp S"
-    proof (cases "a \<in> atom ` S")
-      assume "a \<in> atom ` S"
-      then have "\<forall>b \<in> UNIV - S. (a \<rightleftharpoons> atom b) \<bullet> S \<noteq> S"
-	apply(clarify)
-	
-      show "a \<in> supp S"
-  }
-  then show "supp S = UNIV" by auto
-qed
-*)
-
 
 section {* Automatic instantiation of class @{text at}. *}
 
diff -r 9ae285ce814e -r 08c3ef07cef7 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/Nominal2.thy	Mon May 19 11:19:48 2014 +0100
@@ -700,41 +700,38 @@
 ML {* 
 (* nominal datatype parser *)
 local
-  structure P = Parse;
-  structure S = Scan
-
   fun triple1 ((x, y), z) = (x, y, z)
   fun triple2 ((x, y), z) = (y, x, z)
   fun tuple2 (((x, y), z), u) = (x, y, u, z)
   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
 in
 
-val opt_name = Scan.option (P.binding --| Args.colon)
+val opt_name = Scan.option (Parse.binding --| Args.colon)
 
-val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ
+val anno_typ = Scan.option (Parse.name --| @{keyword "::"}) -- Parse.typ
 
 val bind_mode = @{keyword "binds"} |--
-  S.optional (Args.parens 
+  Scan.optional (Args.parens 
     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
 
 val bind_clauses = 
-  P.enum "," (bind_mode -- S.repeat1 P.term -- (@{keyword "in"} |-- S.repeat1 P.name) >> triple1)
+  Parse.enum "," (bind_mode -- Scan.repeat1 Parse.term -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) >> triple1)
 
 val cnstr_parser =
-  P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2
+  Parse.binding -- Scan.repeat anno_typ -- bind_clauses -- Parse.opt_mixfix >> tuple2
 
 (* datatype parser *)
 val dt_parser =
-  (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- 
-    (@{keyword "="} |-- P.enum1 "|" cnstr_parser)
+  (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix >> triple2) -- 
+    (@{keyword "="} |-- Parse.enum1 "|" cnstr_parser)
 
 (* binding function parser *)
 val bnfun_parser = 
-  S.optional (@{keyword "binder"} |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
+  Scan.optional (@{keyword "binder"} |-- Parse.fixes -- Parse_Spec.where_alt_specs) ([], [])
 
 (* main parser *)
 val main_parser =
-  opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3
+  opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3
 
 end
 
diff -r 9ae285ce814e -r 08c3ef07cef7 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon May 19 11:19:48 2014 +0100
@@ -2167,7 +2167,8 @@
 proof -
   have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
   also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
-  also have "... = supp (set_of M)" by (simp add: supp_of_finite_sets)
+  also have "... = supp (set_of M)"
+    by (simp add: supp_of_finite_sets)
   also have " ... \<subseteq> supp M" by (rule supp_set_of)
   finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
 qed
@@ -2953,7 +2954,6 @@
 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm =>
   case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
     let  
-
       fun first_is_neg lhs rhs [] = NONE
         | first_is_neg lhs rhs (thm::thms) =
           (case Thm.prop_of thm of
@@ -2976,8 +2976,6 @@
          |> map (simplify (put_simpset HOL_basic_ss  ctxt addsimps simp_thms))
          |> map HOLogic.conj_elims
          |> flat
-
-       
     in 
       case first_is_neg lhs rhs prems of
         SOME(thm) => SOME(thm RS @{thm Eq_TrueI})
diff -r 9ae285ce814e -r 08c3ef07cef7 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/nominal_function.ML	Mon May 19 11:19:48 2014 +0100
@@ -181,7 +181,7 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        val _ = Proof_Display.print_consts do_print 
+        val _ = Proof_Display.print_consts do_print
           (Position.thread_data ()) lthy (K false) (map fst fixes)
       in
         (info, 
@@ -265,7 +265,7 @@
      || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant))
 
   fun config_parser default =
-    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
+    (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
      >> (fn opts => fold apply_opt opts default)
 in
   fun nominal_function_parser default_cfg =