# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272984252 -7200
# Node ID c615095827e9b0aa3ddad16e70ef5041aab038bd
# Parent  5aa5c87f7fc039e60fefe6cc03c3c20d3ffe8c8d
Move LF to NewParser. Just works.

diff -r 5aa5c87f7fc0 -r c615095827e9 Nominal/Ex/ExLF.thy
--- a/Nominal/Ex/ExLF.thy	Tue May 04 16:42:36 2010 +0200
+++ b/Nominal/Ex/ExLF.thy	Tue May 04 16:44:12 2010 +0200
@@ -1,5 +1,5 @@
 theory ExLF
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
@@ -7,16 +7,16 @@
 
 nominal_datatype kind =
     Type
-  | KPi "ty" n::"name" k::"kind" bind n in k
+  | KPi "ty" n::"name" k::"kind" bind_set n in k
 and ty =
     TConst "ident"
   | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty" bind n in t
+  | TPi "ty" n::"name" t::"ty" bind_set n in t
 and trm =
     Const "ident"
   | Var "name"
   | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm" bind n in t
+  | Lam "ty" n::"name" t::"trm" bind_set n in t
 
 thm kind_ty_trm.supp