| changeset 19687 | 0a7c6d78ad6b | 
| parent 19564 | d3e2f532459a | 
| child 19972 | 89c5afe4139a | 
--- a/src/HOL/Nominal/Examples/SN.thy Sat May 20 23:36:55 2006 +0200 +++ b/src/HOL/Nominal/Examples/SN.thy Sat May 20 23:36:56 2006 +0200 @@ -167,7 +167,7 @@ TVar "string" | TArr "ty" "ty" (infix "\<rightarrow>" 200) -primrec +primrec (unchecked) "pi\<bullet>(TVar s) = TVar s" "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"