# HG changeset patch
# User haftmann
# Date 1281551144 -7200
# Node ID 07c33be08476a7befced61ff3ca57d1dc02ef593
# Parent  fed4e71a8c0f2729b9f7481dd38ffd02ff559c9a# Parent  1ad96229b455dc01a4269ccf48d340402aa13599
merged

diff -r 1ad96229b455 -r 07c33be08476 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -97,7 +97,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string option -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -114,7 +114,7 @@
   with operations on expecting a regular @{text "ctxt:"}~@{ML_type
   Proof.context}.
 
-  \item @{ML Theory_Target.init}~@{text "NONE thy"} initializes a
+  \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a
   trivial local theory from the given background theory.
   Alternatively, @{text "SOME name"} may be given to initialize a
   @{command locale} or @{command class} context (a fully-qualified
diff -r 1ad96229b455 -r 07c33be08476 doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Wed Aug 11 17:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Wed Aug 11 20:25:44 2010 +0200
@@ -123,7 +123,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
-  \indexdef{}{ML}{Theory\_Target.init}\verb|Theory_Target.init: string option -> theory -> local_theory| \\[1ex]
+  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex]
   \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
 \verb|    local_theory -> (term * (string * thm)) * local_theory| \\
   \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
@@ -139,7 +139,7 @@
   any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
   with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
 
-  \item \verb|Theory_Target.init|~\isa{NONE\ thy} initializes a
+  \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a
   trivial local theory from the given background theory.
   Alternatively, \isa{SOME\ name} may be given to initialize a
   \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -9,17 +9,16 @@
 imports Main
 begin
 
-definition "cd" :: "[nat, nat, nat] => bool" where
-  "cd x m n  == x dvd m & x dvd n"
-
-definition gcd     :: "[nat, nat] => nat" where
-  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+definition "cd" :: "[nat, nat, nat] => bool"
+  where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
 
-consts fac     :: "nat => nat"
+definition gcd :: "[nat, nat] => nat"
+  where "gcd m n = (SOME x. cd x m n & (!y.(cd y m n) --> y<=x))"
 
-primrec
+primrec fac :: "nat => nat"
+where
   "fac 0 = Suc 0"
-  "fac(Suc n) = (Suc n)*fac(n)"
+| "fac (Suc n) = Suc n * fac n"
 
 
 subsubsection {* cd *}
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Heap.thy
--- a/src/HOL/Hoare/Heap.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Heap.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -57,8 +57,8 @@
 
 subsection "Non-repeating paths"
 
-definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
-  "distPath h x as y   \<equiv>   Path h x as y  \<and>  distinct as"
+definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
+  where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
 
 text{* The term @{term"distPath h x as y"} expresses the fact that a
 non-repeating path @{term as} connects location @{term x} to location
@@ -82,8 +82,8 @@
 
 subsubsection "Relational abstraction"
 
-definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool" where
-"List h x as == Path h x as Null"
+definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "List h x as = Path h x as Null"
 
 lemma [simp]: "List h x [] = (x = Null)"
 by(simp add:List_def)
@@ -133,11 +133,11 @@
 
 subsection "Functional abstraction"
 
-definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool" where
-"islist h p == \<exists>as. List h p as"
+definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
+  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
 
-definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list" where
-"list h p == SOME as. List h p as"
+definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+  where "list h p = (SOME as. List h p as)"
 
 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
 apply(simp add:islist_def list_def)
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -41,8 +41,8 @@
   "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
   "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
-  "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
 
 
 
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -216,18 +216,19 @@
 
 text"This is still a bit rough, especially the proof."
 
-definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cor P Q == if P then True else Q"
+definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "cor P Q \<longleftrightarrow> (if P then True else Q)"
 
-definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cand P Q == if P then Q else False"
+definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "cand P Q \<longleftrightarrow> (if P then Q else False)"
 
-fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
-"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
-                                else y # merge(x#xs,ys,f))" |
-"merge(x#xs,[],f) = x # merge(xs,[],f)" |
-"merge([],y#ys,f) = y # merge([],ys,f)" |
-"merge([],[],f) = []"
+fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
+where
+  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
+                                  else y # merge(x#xs,ys,f))"
+| "merge(x#xs,[],f) = x # merge(xs,[],f)"
+| "merge([],y#ys,f) = y # merge([],ys,f)"
+| "merge([],[],f) = []"
 
 text{* Simplifies the proof a little: *}
 
@@ -336,8 +337,9 @@
 Path}. Since the result is not that convincing, we do not prove any of
 the lemmas.*}
 
-consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
-       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+axiomatization
+  ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
+  path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
 
 text"First some basic lemmas:"
 
@@ -479,8 +481,8 @@
 
 subsection "Storage allocation"
 
-definition new :: "'a set \<Rightarrow> 'a" where
-"new A == SOME a. a \<notin> A"
+definition new :: "'a set \<Rightarrow> 'a"
+  where "new A = (SOME a. a \<notin> A)"
 
 
 lemma new_notin:
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Pointers0.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -44,11 +44,10 @@
 
 subsection "Paths in the heap"
 
-consts
- Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
+primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  "Path h x [] y = (x = y)"
+| "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
 
 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
 apply(case_tac xs)
@@ -73,8 +72,8 @@
 
 subsubsection "Relational abstraction"
 
-definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where
-"List h x as == Path h x as Null"
+definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "List h x as = Path h x as Null"
 
 lemma [simp]: "List h x [] = (x = Null)"
 by(simp add:List_def)
@@ -121,11 +120,11 @@
 
 subsection "Functional abstraction"
 
-definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where
-"islist h p == \<exists>as. List h p as"
+definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
+  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
 
-definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
-"list h p == SOME as. List h p as"
+definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
+  where "list h p = (SOME as. List h p as)"
 
 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
 apply(simp add:islist_def list_def)
@@ -404,8 +403,8 @@
 
 subsection "Storage allocation"
 
-definition new :: "'a set \<Rightarrow> 'a::ref" where
-"new A == SOME a. a \<notin> A & a \<noteq> Null"
+definition new :: "'a set \<Rightarrow> 'a::ref"
+  where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
 
 
 lemma new_notin:
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/README.html
--- a/src/HOL/Hoare/README.html	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/README.html	Wed Aug 11 20:25:44 2010 +0200
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/SchorrWaite.thy
-    ID:         $Id$
     Author:     Farhad Mehta
     Copyright   2003 TUM
 
@@ -146,14 +145,15 @@
  apply(simp add:fun_upd_apply S_def)+
 done
 
-consts
+primrec
   --"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
   stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
-primrec
-stkOk_nil:  "stkOk c l r iL iR t [] = True"
-stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
-                                  iL p = (if c p then l p else t) \<and>
-                                  iR p = (if c p then t else r p))"
+where
+  stkOk_nil:  "stkOk c l r iL iR t [] = True"
+| stkOk_cons:
+    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
+      iL p = (if c p then l p else t) \<and>
+      iR p = (if c p then t else r p))"
 
 text {* Rewrite rules for stkOk *}
 
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/Heap.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
@@ -18,11 +17,10 @@
 
 subsection "Paths in the heap"
 
-consts
- Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
+primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "Path h x [] y = (x = y)"
+| "Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
 
 lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
 by (cases xs) simp_all
@@ -41,8 +39,8 @@
 
 subsection "Lists on the heap"
 
-definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" where
-"List h x as == Path h x as 0"
+definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
+  where "List h x as = Path h x as 0"
 
 lemma [simp]: "List h x [] = (x = 0)"
 by (simp add: List_def)
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Separation.thy	Wed Aug 11 20:25:44 2010 +0200
@@ -16,20 +16,20 @@
 
 text{* The semantic definition of a few connectives: *}
 
-definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) where
-"h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
+definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
+  where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
 
-definition is_empty :: "heap \<Rightarrow> bool" where
-"is_empty h == h = empty"
+definition is_empty :: "heap \<Rightarrow> bool"
+  where "is_empty h \<longleftrightarrow> h = empty"
 
-definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
-"singl h x y == dom h = {x} & h x = Some y"
+definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
 
-definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
-"star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
+definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+  where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)"
 
-definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
-"wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
+definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+  where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))"
 
 text{*This is what assertions look like without any syntactic sugar: *}
 
diff -r 1ad96229b455 -r 07c33be08476 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -830,10 +830,10 @@
           str "case Seq.pull (testf p) of", Pretty.brk 1,
           str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
           str " =>", Pretty.brk 1, str "SOME ",
-          Pretty.block (str "[" ::
-            Pretty.commas (map (fn (s, T) => Pretty.block
-              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
-            [str "]"]), Pretty.brk 1,
+          Pretty.enum "," "[" "]"
+            (map (fn (s, T) => Pretty.block
+              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
+          Pretty.brk 1,
           str "| NONE => NONE);"]) ^
       "\n\nend;\n";
     val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -16,7 +16,6 @@
   val defined: theory -> string -> bool
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
-  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val map_specs: ('a -> 'att) ->
     (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
   val map_facts: ('a -> 'att) ->
@@ -25,6 +24,7 @@
   val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
+  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val crude_closure: Proof.context -> src -> src
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -94,8 +94,7 @@
 
 fun pretty_attribs _ [] = []
   | pretty_attribs ctxt srcs =
-      [Pretty.enclose "[" "]"
-        (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
+      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
 
 
 (* get attributes *)
@@ -115,11 +114,6 @@
 
 fun attribute thy = attribute_i thy o intern_src thy;
 
-fun eval_thms ctxt args = ProofContext.note_thmss ""
-    [(Thm.empty_binding, args |> map (fn (a, atts) =>
-        (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
-  |> fst |> maps snd;
-
 
 (* attributed declarations *)
 
@@ -129,6 +123,15 @@
 fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
 
 
+(* fact expressions *)
+
+fun eval_thms ctxt srcs = ctxt
+  |> ProofContext.note_thmss ""
+    (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
+      [((Binding.empty, []), srcs)])
+  |> fst |> maps snd;
+
+
 (* crude_closure *)
 
 (*Produce closure without knowing facts in advance! The following
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/calculation.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -37,8 +37,10 @@
     ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
 );
 
+val get_rules = #1 o Data.get o Context.Proof;
+
 fun print_rules ctxt =
-  let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
+  let val (trans, sym) = get_rules ctxt in
     [Pretty.big_list "transitivity rules:"
         (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
       Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
@@ -122,21 +124,21 @@
 
 (* also and finally *)
 
-val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
-
 fun calculate prep_rules final raw_rules int state =
   let
+    val ctxt = Proof.context_of state;
+
     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
     fun projection ths th = exists (curry eq_prop th) ths;
 
-    val opt_rules = Option.map (prep_rules state) raw_rules;
+    val opt_rules = Option.map (prep_rules ctxt) raw_rules;
     fun combine ths =
       (case opt_rules of SOME rules => rules
       | NONE =>
           (case ths of
-            [] => Item_Net.content (#1 (get_rules state))
-          | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
+            [] => Item_Net.content (#1 (get_rules ctxt))
+          | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
       |> Seq.filter (not o projection ths);
 
@@ -154,9 +156,9 @@
   end;
 
 val also = calculate (K I) false;
-val also_cmd = calculate Proof.get_thmss_cmd false;
+val also_cmd = calculate Attrib.eval_thms false;
 val finally = calculate (K I) true;
-val finally_cmd = calculate Proof.get_thmss_cmd true;
+val finally_cmd = calculate Attrib.eval_thms true;
 
 
 (* moreover and ultimately *)
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/class.ML
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/class_declaration.ML
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -416,7 +416,7 @@
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   Thm_Deps.thm_deps (Toplevel.theory_of state)
-    (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
+    (Attrib.eval_thms (Toplevel.context_of state) args));
 
 
 (* find unused theorems *)
@@ -450,20 +450,20 @@
 
 local
 
-fun string_of_stmts state args =
-  Proof.get_thmss_cmd state args
-  |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
+fun string_of_stmts ctxt args =
+  Attrib.eval_thms ctxt args
+  |> map (Element.pretty_statement ctxt Thm.theoremK)
   |> Pretty.chunks2 |> Pretty.string_of;
 
-fun string_of_thms state args =
-  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
+fun string_of_thms ctxt args =
+  Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
 
 fun string_of_prfs full state arg =
   Pretty.string_of
     (case arg of
       NONE =>
         let
-          val {context = ctxt, goal = thm} = Proof.simple_goal state;
+          val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
           val thy = ProofContext.theory_of ctxt;
           val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
@@ -472,20 +472,19 @@
           Proof_Syntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
         end
-    | SOME args => Pretty.chunks
-        (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
-          (Proof.get_thmss_cmd state args)));
+    | SOME srcs =>
+        let val ctxt = Toplevel.context_of state
+        in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
+        |> Pretty.chunks);
 
-fun string_of_prop state s =
+fun string_of_prop ctxt s =
   let
-    val ctxt = Proof.context_of state;
     val prop = Syntax.read_prop ctxt s;
     val ctxt' = Variable.auto_fixes prop ctxt;
   in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
 
-fun string_of_term state s =
+fun string_of_term ctxt s =
   let
-    val ctxt = Proof.context_of state;
     val t = Syntax.read_term ctxt s;
     val T = Term.type_of t;
     val ctxt' = Variable.auto_fixes t ctxt;
@@ -495,24 +494,21 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
   end;
 
-fun string_of_type state s =
-  let
-    val ctxt = Proof.context_of state;
-    val T = Syntax.read_typ ctxt s;
+fun string_of_type ctxt s =
+  let val T = Syntax.read_typ ctxt s
   in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
 
 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
-  Print_Mode.with_modes modes (fn () =>
-    writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
+  Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
 
 in
 
-val print_stmts = print_item string_of_stmts;
-val print_thms = print_item string_of_thms;
+val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
+val print_thms = print_item (string_of_thms o Toplevel.context_of);
 val print_prfs = print_item o string_of_prfs;
-val print_prop = print_item string_of_prop;
-val print_term = print_item string_of_term;
-val print_type = print_item string_of_type;
+val print_prop = print_item (string_of_prop o Toplevel.context_of);
+val print_term = print_item (string_of_term o Toplevel.context_of);
+val print_type = print_item (string_of_type o Toplevel.context_of);
 
 end;
 
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -60,7 +60,6 @@
   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
-  val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss: ((thm list * attribute list) list) list -> state -> state
@@ -679,8 +678,6 @@
 
 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
-fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
-
 end;
 
 
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -1123,7 +1123,7 @@
 val type_notation = gen_notation (K type_syntax);
 val notation = gen_notation const_syntax;
 
-fun target_type_notation add  mode args phi =
+fun target_type_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (T, mx) =>
       let
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -20,7 +20,6 @@
   val theory_of: state -> theory
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
-  val enter_proof_body: state -> Proof.state
   val end_theory: Position.T -> state -> theory
   val print_state_context: state -> unit
   val print_state: bool -> state -> unit
@@ -188,8 +187,6 @@
     Proof (prf, _) => Proof_Node.position prf
   | _ => raise UNDEF);
 
-val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
-
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
   | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
 
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -75,8 +75,7 @@
 
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) = Pretty.str x
-  | pretty_ast (Appl asts) =
-      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
+  | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -28,24 +28,13 @@
 (* matching types/consts *)
 
 fun matches_subtype thy typat =
-  let
-    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
-
-    fun fs [] = false
-      | fs (t :: ts) = f t orelse fs ts
+  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
 
-    and f (t as Type (_, ars)) = p t orelse fs ars
-      | f t = p t;
-  in f end;
-
-fun check_const p (nm, (ty, _)) =
-  if p (nm, ty)
-  then SOME (Term.size_of_typ ty)
-  else NONE;
+fun check_const pred (nm, (ty, _)) =
+  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
 
 fun opt_not f (c as (_, (ty, _))) =
-  if is_some (f c)
-  then NONE else SOME (Term.size_of_typ ty);
+  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
 
 fun filter_const _ NONE = NONE
   | filter_const f (SOME (c, r)) =
@@ -71,8 +60,7 @@
     val ty' = Logic.unvarifyT_global ty;
   in
     Pretty.block
-     [Pretty.quote (Pretty.str nm), Pretty.fbrk,
-      Pretty.str "::", Pretty.brk 1,
+     [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
       Pretty.quote (Syntax.pretty_typ ctxt ty')]
   end;
 
@@ -128,35 +116,35 @@
 
     val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
-    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
-      :: Pretty.str ""
-      :: (Pretty.str o implode)
-           (if null matches
-            then ["nothing found", end_msg]
-            else ["found ", (string_of_int o length) matches,
-                  " constants", end_msg, ":"])
-      :: Pretty.str ""
-      :: map (pretty_const ctxt) matches
-    |> Pretty.chunks
-    |> Pretty.writeln
-  end;
+    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
+    Pretty.str "" ::
+    Pretty.str
+     (if null matches
+      then "nothing found" ^ end_msg
+      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
+    Pretty.str "" ::
+    map (pretty_const ctxt) matches
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 (* command syntax *)
 
-fun find_consts_cmd spec =
-  Toplevel.unknown_theory o Toplevel.keep (fn state =>
-    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
+local
 
 val criterion =
   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   Parse.xname >> Loose;
 
+in
+
 val _ =
   Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
     (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
-      >> (Toplevel.no_timing oo find_consts_cmd));
+      >> (fn spec => Toplevel.no_timing o
+        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
 
 end;
 
+end;
+
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -433,36 +433,27 @@
 
     val tally_msg =
       (case foundo of
-        NONE => "displaying " ^ string_of_int returned ^ " theorems"
+        NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
       | SOME found =>
-          "found " ^ string_of_int found ^ " theorems" ^
+          "found " ^ string_of_int found ^ " theorem(s)" ^
             (if returned < found
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
 
     val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
-    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
-        :: Pretty.str "" ::
-     (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
-      else
-        [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
+    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
+    Pretty.str "" ::
+    (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
+     else
+      [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
         map (pretty_thm ctxt) thms)
-    |> Pretty.chunks |> Pretty.writeln
-  end;
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 
 (** command syntax **)
 
-fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
-  Toplevel.unknown_theory o Toplevel.keep (fn state =>
-    let
-      val proof_state = Toplevel.enter_proof_body state;
-      val ctxt = Proof.context_of proof_state;
-      val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
-    in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
-
 local
 
 val criterion =
@@ -486,7 +477,13 @@
   Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
     Keyword.diag
     (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
-      >> (Toplevel.no_timing oo find_theorems_cmd));
+      >> (fn ((opt_lim, rem_dups), spec) =>
+        Toplevel.no_timing o
+        Toplevel.keep (fn state =>
+          let
+            val ctxt = Toplevel.context_of state;
+            val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
+          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
 
 end;
 
diff -r 1ad96229b455 -r 07c33be08476 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/codegen.ML	Wed Aug 11 20:25:44 2010 +0200
@@ -889,9 +889,8 @@
               mk_app false (str "testf") (map (str o fst) args),
               Pretty.brk 1, str "then NONE",
               Pretty.brk 1, str "else ",
-              Pretty.block [str "SOME ", Pretty.block (str "[" ::
-                Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
-                  [str "]"])]]),
+              Pretty.block [str "SOME ",
+                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
           str ");"]) ^
       "\n\nend;\n";
     val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;