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