# HG changeset patch
# User wenzelm
# Date 1193254417 -7200
# Node ID 64e3f45dc6f4b425ccb1950a33a49ed679c44b51
# Parent  7c86f9ed85886b6d8a8a15a2e6cc74555a9523a2
updated;

diff -r 7c86f9ed8588 -r 64e3f45dc6f4 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Wed Oct 24 21:33:37 2007 +0200
@@ -6,7 +6,7 @@
   nulla :: a;
 };
 
-heada :: (Codegen.Null b) => [b] -> b;
+heada :: (Codegen.Null a) => [a] -> a;
 heada (x : xs) = x;
 heada [] = Codegen.nulla;
 
diff -r 7c86f9ed8588 -r 64e3f45dc6f4 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Wed Oct 24 21:33:37 2007 +0200
@@ -11,8 +11,8 @@
 type 'a null = {null : 'a};
 fun null (A_:'a null) = #null A_;
 
-fun head B_ (x :: xs) = x
-  | head B_ [] = null B_;
+fun head A_ (x :: xs) = x
+  | head A_ [] = null A_;
 
 val null_option : 'a option = NONE;
 
diff -r 7c86f9ed8588 -r 64e3f45dc6f4 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Wed Oct 24 21:33:37 2007 +0200
@@ -11,8 +11,8 @@
 type 'a null = {null : 'a};;
 let null _A = _A.null;;
 
-let rec head _B = function x :: xs -> x
-                  | [] -> null _B;;
+let rec head _A = function x :: xs -> x
+                  | [] -> null _A;;
 
 let rec null_option = None;;
 
diff -r 7c86f9ed8588 -r 64e3f45dc6f4 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Wed Oct 24 21:33:37 2007 +0200
@@ -17,11 +17,11 @@
 structure Codegen = 
 struct
 
-fun collect_duplicates B_ xs ys (z :: zs) =
-  (if List.member B_ z xs
-    then (if List.member B_ z ys then collect_duplicates B_ xs ys zs
-           else collect_duplicates B_ xs (z :: ys) zs)
-    else collect_duplicates B_ (z :: xs) (z :: ys) zs)
-  | collect_duplicates B_ xs ys [] = xs;
+fun collect_duplicates A_ xs ys (z :: zs) =
+  (if List.member A_ z xs
+    then (if List.member A_ z ys then collect_duplicates A_ xs ys zs
+           else collect_duplicates A_ xs (z :: ys) zs)
+    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
+  | collect_duplicates A_ xs ys [] = xs;
 
 end; (*struct Codegen*)
diff -r 7c86f9ed8588 -r 64e3f45dc6f4 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Wed Oct 24 21:33:37 2007 +0200
@@ -54,15 +54,15 @@
   Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree |
   Leaf of 'a * 'b;
 
-fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
-  (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_)
+fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
+  (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) A2_)
         it key
-    then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
-    else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
-  | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
-    (if HOL.eqop C1_ it key then Leaf (key, entry)
+    then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
+    else Branch (t1, key, update (A1_, A2_) (it, entry) t2))
+  | update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
+    (if HOL.eqop A1_ it key then Leaf (key, entry)
       else (if HOL.less_eq
-                 ((Orderings.ord_order o Orderings.order_linorder) C2_) it
+                 ((Orderings.ord_order o Orderings.order_linorder) A2_) it
                  key
              then Branch (Leaf (it, entry), it, Leaf (key, vala))
              else Branch (Leaf (key, vala), it, Leaf (it, entry))));
diff -r 7c86f9ed8588 -r 64e3f45dc6f4 doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Wed Oct 24 21:33:37 2007 +0200
@@ -1303,7 +1303,7 @@
 \ findzero{\isachardot}domintros%
 \begin{isamarkuptext}%
 \begin{isabelle}%
-{\isacharparenleft}{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
+{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
 \end{isabelle}
 
   Domain introduction rules allow to show that a given value lies in the