src/HOL/Tools/Quotient/quotient_def.ML
changeset 62953 48d935524988
parent 62775 b486f512a471
child 62956 bb3986d95562
equal deleted inserted replaced
62952:85c6c2a1952d 62953:48d935524988
   143 
   143 
   144     fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
   144     fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
   145     val lhs = prep_term lhs_constraint raw_lhs
   145     val lhs = prep_term lhs_constraint raw_lhs
   146     val rhs = prep_term dummyT raw_rhs
   146     val rhs = prep_term dummyT raw_rhs
   147 
   147 
   148     val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
   148     val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined"
   149     val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
   149     val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
   150     val _ = if is_Const rhs then () else warning "The definiens is not a constant"
   150     val _ = if is_Const rhs then () else warning "The definiens is not a constant"
   151 
   151 
   152     val var =
   152     val var =
   153       (case opt_var of
   153       (case opt_var of