Quot/quotient_def.ML
changeset 1141 3c8ad149a4d3
parent 1138 93c9022ba5e9
child 1142 b102e1444851
equal deleted inserted replaced
1140:aaeb5a34d21a 1141:3c8ad149a4d3
    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