src/HOL/Bali/DeclConcepts.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 35547 991a6af75978
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -1377,7 +1377,7 @@
     1.4    fspec = "vname \<times> qtname"
     1.5  
     1.6  translations 
     1.7 -  "fspec" <= (type) "vname \<times> qtname" 
     1.8 +  (type) "fspec" <= (type) "vname \<times> qtname" 
     1.9  
    1.10  definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
    1.11  "imethds G I