# HG changeset patch
# User wenzelm
# Date 1362058194 -3600
# Node ID 337cfc42c9c803cef86ce8987f60b2c8b6c735b2
# Parent  d2aeb3dffb8f5feb37ccd7de43b22b3bc5f184a1
eliminated legacy 'axioms';

diff -r d2aeb3dffb8f -r 337cfc42c9c8 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Thu Feb 28 14:24:21 2013 +0100
+++ b/src/HOL/Prolog/Test.thy	Thu Feb 28 14:29:54 2013 +0100
@@ -26,52 +26,51 @@
 
 typedecl person
 
-consts
-  append  :: "['a list, 'a list, 'a list]            => bool"
-  reverse :: "['a list, 'a list]                     => bool"
+axiomatization
+  append  :: "['a list, 'a list, 'a list]            => bool" and
+  reverse :: "['a list, 'a list]                     => bool" and
 
-  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
-  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool"
+  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool" and
+  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool" and
 
-  bob     :: person
-  sue     :: person
-  ned     :: person
+  bob     :: person and
+  sue     :: person and
+  ned     :: person and
 
-  nat23   :: nat          ("23")
-  nat24   :: nat          ("24")
-  nat25   :: nat          ("25")
+  nat23   :: nat          ("23") and
+  nat24   :: nat          ("24") and
+  nat25   :: nat          ("25") and
 
-  age     :: "[person, nat]                          => bool"
+  age     :: "[person, nat]                          => bool" and
 
-  eq      :: "['a, 'a]                               => bool"
+  eq      :: "['a, 'a]                               => bool" and
 
-  empty   :: "['b]                                   => bool"
-  add     :: "['a, 'b, 'b]                           => bool"
-  remove  :: "['a, 'b, 'b]                           => bool"
+  empty   :: "['b]                                   => bool" and
+  add     :: "['a, 'b, 'b]                           => bool" and
+  remove  :: "['a, 'b, 'b]                           => bool" and
   bag_appl:: "['a, 'a, 'a, 'a]                       => bool"
-
-axioms
-        append:  "append  []    xs  xs    ..
-                  append (x#xs) ys (x#zs) :- append xs ys zs"
-        reverse: "reverse L1 L2 :- (!rev_aux.
+where
+        append:  "\<And>x xs ys zs. append  []    xs  xs    ..
+                  append (x#xs) ys (x#zs) :- append xs ys zs" and
+        reverse: "\<And>L1 L2. reverse L1 L2 :- (!rev_aux.
                   (!L.          rev_aux  []    L  L )..
                   (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
-                  => rev_aux L1 L2 [])"
+                  => rev_aux L1 L2 [])" and
 
-        mappred: "mappred P  []     []    ..
-                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
-        mapfun:  "mapfun f  []     []      ..
-                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
+        mappred: "\<And>x xs y ys P. mappred P  []     []    ..
+                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys" and
+        mapfun:  "\<And>x xs ys f. mapfun f  []     []      ..
+                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" and
 
         age:     "age bob 24 ..
                   age sue 23 ..
-                  age ned 23"
+                  age ned 23" and
 
-        eq:      "eq x x"
+        eq:      "\<And>x. eq x x" and
 
 (* actual definitions of empty and add is hidden -> yields abstract data type *)
 
-        bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
+        bag_appl: "\<And>A B X Y. bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
                                 empty    S1    &
                                 add A    S1 S2 &
                                 add B    S2 S3 &
diff -r d2aeb3dffb8f -r 337cfc42c9c8 src/HOL/Prolog/Type.thy
--- a/src/HOL/Prolog/Type.thy	Thu Feb 28 14:24:21 2013 +0100
+++ b/src/HOL/Prolog/Type.thy	Thu Feb 28 14:29:54 2013 +0100
@@ -10,14 +10,13 @@
 
 typedecl ty
 
-consts
-  bool    :: ty
-  nat     :: ty
-  arrow   :: "ty => ty => ty"       (infixr "->" 20)
-  typeof  :: "[tm, ty] => bool"
+axiomatization
+  bool    :: ty and
+  nat     :: ty and
+  arrow   :: "ty => ty => ty"       (infixr "->" 20) and
+  typeof  :: "[tm, ty] => bool" and
   anyterm :: tm
-
-axioms  common_typeof:   "
+where common_typeof:   "
 typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
 
 typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
@@ -35,13 +34,13 @@
 typeof (M - N) nat :- typeof M nat & typeof N nat..
 typeof (M * N) nat :- typeof M nat & typeof N nat"
 
-axioms good_typeof:     "
+axiomatization where good_typeof:     "
 typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
 
-axioms bad1_typeof:     "
+axiomatization where bad1_typeof:     "
 typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
 
-axioms bad2_typeof:     "
+axiomatization where bad2_typeof:     "
 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"