equal
deleted
inserted
replaced
385 if not (null us) then |
385 if not (null us) then |
386 raise FO_TERM [u] (* only "tconst"s have type arguments *) |
386 raise FO_TERM [u] (* only "tconst"s have type arguments *) |
387 else case strip_prefix_and_unascii tfree_prefix a of |
387 else case strip_prefix_and_unascii tfree_prefix a of |
388 SOME b => make_tfree ctxt b |
388 SOME b => make_tfree ctxt b |
389 | NONE => |
389 | NONE => |
390 case strip_prefix_and_unascii tvar_prefix a of |
390 (* Could be an Isabelle variable or a variable from the ATP, say "X1" |
391 SOME b => make_tvar b |
391 or "_5018". Sometimes variables from the ATP are indistinguishable |
392 | NONE => |
392 from Isabelle variables, which forces us to use a type parameter in |
393 (* Variable from the ATP, say "X1" *) |
393 all cases. *) |
394 Type_Infer.param 0 (a, HOLogic.typeS) |
394 (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS) |
|
395 |> Type_Infer.param 0 |
395 end |
396 end |
396 |
397 |
397 (* Type class literal applied to a type. Returns triple of polarity, class, |
398 (* Type class literal applied to a type. Returns triple of polarity, class, |
398 type. *) |
399 type. *) |
399 fun type_constraint_from_term ctxt (u as ATerm (a, us)) = |
400 fun type_constraint_from_term ctxt (u as ATerm (a, us)) = |