src/Pure/consts.ML
changeset 21822 5a279c9138b6
parent 21794 1a9f57f1bc3a
child 22559 b824487d9b41
equal deleted inserted replaced
21821:7fa19d17f488 21822:5a279c9138b6
   262 
   262 
   263 fun abbreviate pp tsig naming mode (c, raw_rhs) consts =
   263 fun abbreviate pp tsig naming mode (c, raw_rhs) consts =
   264   let
   264   let
   265     val cert_term = certify pp tsig (consts |> set_expand false);
   265     val cert_term = certify pp tsig (consts |> set_expand false);
   266     val expand_term = certify pp tsig (consts |> set_expand true);
   266     val expand_term = certify pp tsig (consts |> set_expand true);
   267     val force_expand = (mode = #1 Syntax.internal_mode);
   267     val force_expand = mode = Syntax.internalM;
   268 
   268 
   269     val rhs = raw_rhs
   269     val rhs = raw_rhs
   270       |> Term.map_types (Type.cert_typ tsig)
   270       |> Term.map_types (Type.cert_typ tsig)
   271       |> cert_term;
   271       |> cert_term;
   272     val T = Term.fastype_of rhs;
   272     val T = Term.fastype_of rhs;