equal
deleted
inserted
replaced
36 Restriction: At the moment the right-hand side of the |
36 Restriction: At the moment the right-hand side of the |
37 definition must be a constant. Similarly the left-hand |
37 definition must be a constant. Similarly the left-hand |
38 side must be a constant. |
38 side must be a constant. |
39 *) |
39 *) |
40 fun error_msg bind str = |
40 fun error_msg bind str = |
|
41 let |
|
42 val name = Binding.name_of bind |
|
43 val pos = Position.str_of (Binding.pos_of bind) |
|
44 in |
41 error ("Head of quotient_definition " ^ |
45 error ("Head of quotient_definition " ^ |
42 (quote str) ^ " differs from declaration " ^ (Binding.name_of bind) ^ |
46 (quote str) ^ " differs from declaration " ^ name ^ pos) |
43 Position.str_of (Binding.pos_of bind)) |
47 end |
44 |
48 |
45 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
49 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
46 let |
50 let |
47 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
51 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
48 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
52 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |