src/HOL/MiniML/I.thy

--- a/src/HOL/MiniML/I.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/MiniML/I.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -11,11 +11,11 @@
         I :: [expr, typ list, nat, subst] => result_W
 
 primrec I expr
-        I_Var   "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
+        "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
                                     else Fail)"
-        I_Abs   "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+        "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
                                      Ok(s, TVar n -> t, m) )"
-        I_App   "I (App e1 e2) a n s =
+        "I (App e1 e2) a n s =
                    ( (s1,t1,m1) := I e1 a n s;
                      (s2,t2,m2) := I e2 a m1 s1;
                      u := mgu ($s2 t1) ($s2 t2 -> TVar m2);