equal
deleted
inserted
replaced
71 |
71 |
72 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
72 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
73 let |
73 let |
74 val lhs = Syntax.read_term lthy lhs_str |
74 val lhs = Syntax.read_term lthy lhs_str |
75 val rhs = Syntax.read_term lthy rhs_str |
75 val rhs = Syntax.read_term lthy rhs_str |
76 (* FIXME: Relating the reads will cause errors. *) |
76 val lthy' = Variable.declare_term lhs lthy |
|
77 val lthy'' = Variable.declare_term rhs lthy' |
77 in |
78 in |
78 quotient_def mx attr lhs rhs lthy |> snd |
79 quotient_def mx attr lhs rhs lthy'' |> snd |
79 end |
80 end |
80 |
81 |
81 val _ = OuterKeyword.keyword "as"; |
82 val _ = OuterKeyword.keyword "as"; |
82 |
83 |
83 val quotdef_parser = |
84 val quotdef_parser = |