equal
deleted
inserted
replaced
69 ((trm, thm), lthy'') |
69 ((trm, thm), lthy'') |
70 end |
70 end |
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, rhs] = Syntax.read_terms lthy [lhs_str, rhs_str] |
74 val lhs = Syntax.read_term lthy lhs_str |
|
75 val rhs = Syntax.read_term lthy rhs_str |
75 val lthy' = Variable.declare_term lhs lthy |
76 val lthy' = Variable.declare_term lhs lthy |
76 val lthy'' = Variable.declare_term rhs 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 |