src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Wed Aug 18 20:45:18 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Aug 18 20:45:52 1999 +0200
@@ -39,7 +39,7 @@
     else ();
     state'
     |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
-    |> Proof.assm_i (refl_tac, refl_tac) name atts [(eq, ([], []))]
+    |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(eq, ([], []))])]
   end;
 
 val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;