changeset 10464 | b7b916a82dca |
parent 9467 | 52fb37876254 |
child 11718 | 92706a69dacc |
--- a/src/Pure/Isar/local_defs.ML Mon Nov 13 21:59:49 2000 +0100 +++ b/src/Pure/Isar/local_defs.ML Mon Nov 13 22:01:07 2000 +0100 @@ -63,7 +63,7 @@ state |> fix [([x], None)] |> Proof.match_bind_i [(pats, rhs)] - |> Proof.assm_i export_defs [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])] + |> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] end; val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;