# HG changeset patch
# User wenzelm
# Date 1148161013 -7200
# Node ID 4477003648cc4d3626e2e08fc42aa8dbd1cb544f
# Parent  6101fbebda1d3a829d84737198bbed046f7142fb
ax_derivs: precise typing;

diff -r 6101fbebda1d -r 4477003648cc src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sat May 20 23:36:51 2006 +0200
+++ b/src/HOL/Bali/AxSem.thy	Sat May 20 23:36:53 2006 +0200
@@ -435,7 +435,7 @@
                                                 (   "_\<Turnstile>_:_" [61,0, 58] 57)
     ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
                                                 ("_,_|\<Turnstile>_"   [61,58,58] 57)
-    ax_derivs :: "prog \<Rightarrow> ('b triples \<times> 'a triples) set"
+    ax_derivs :: "prog \<Rightarrow> ('a triples \<times> 'a triples) set"
 
 syntax