src/HOL/Tools/ATP/atp_reconstruct.ML
changeset 45511 9b0f8ca4388e
parent 45379 0147a4348ca1
child 45519 cd6e78cb6ee8
     1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Nov 15 22:13:39 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Nov 15 22:13:39 2011 +0100
     1.3 @@ -283,26 +283,26 @@
     1.4     constrained by information from type literals, or by type inference. *)
     1.5  fun typ_from_atp ctxt (u as ATerm (a, us)) =
     1.6    let val Ts = map (typ_from_atp ctxt) us in
     1.7 -    case strip_prefix_and_unascii type_const_prefix a of
     1.8 +    case unprefix_and_unascii type_const_prefix a of
     1.9        SOME b => Type (invert_const b, Ts)
    1.10      | NONE =>
    1.11        if not (null us) then
    1.12          raise HO_TERM [u]  (* only "tconst"s have type arguments *)
    1.13 -      else case strip_prefix_and_unascii tfree_prefix a of
    1.14 +      else case unprefix_and_unascii tfree_prefix a of
    1.15          SOME b => make_tfree ctxt b
    1.16        | NONE =>
    1.17          (* Could be an Isabelle variable or a variable from the ATP, say "X1"
    1.18             or "_5018". Sometimes variables from the ATP are indistinguishable
    1.19             from Isabelle variables, which forces us to use a type parameter in
    1.20             all cases. *)
    1.21 -        (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS)
    1.22 +        (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)
    1.23          |> Type_Infer.param 0
    1.24    end
    1.25  
    1.26  (* Type class literal applied to a type. Returns triple of polarity, class,
    1.27     type. *)
    1.28  fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
    1.29 -  case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
    1.30 +  case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
    1.31      (SOME b, [T]) => (b, T)
    1.32    | _ => raise HO_TERM [u]
    1.33  
    1.34 @@ -335,6 +335,8 @@
    1.35  fun num_type_args thy s =
    1.36    if String.isPrefix skolem_const_prefix s then
    1.37      s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
    1.38 +  else if String.isPrefix lambda_lifted_prefix s then
    1.39 +    if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0
    1.40    else
    1.41      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.42  
    1.43 @@ -364,7 +366,7 @@
    1.44              else
    1.45                list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
    1.46            end
    1.47 -        else case strip_prefix_and_unascii const_prefix s of
    1.48 +        else case unprefix_and_unascii const_prefix s of
    1.49            SOME s' =>
    1.50            let
    1.51              val ((s', s''), mangled_us) =
    1.52 @@ -429,12 +431,10 @@
    1.53                  SOME T => map slack_fastype_of term_ts ---> T
    1.54                | NONE => map slack_fastype_of ts ---> HOLogic.typeT
    1.55              val t =
    1.56 -              case strip_prefix_and_unascii fixed_var_prefix s of
    1.57 -                SOME s =>
    1.58 -                (* FIXME: reconstruction of lambda-lifting *)
    1.59 -                Free (s, T)
    1.60 +              case unprefix_and_unascii fixed_var_prefix s of
    1.61 +                SOME s => Free (s, T)
    1.62                | NONE =>
    1.63 -                case strip_prefix_and_unascii schematic_var_prefix s of
    1.64 +                case unprefix_and_unascii schematic_var_prefix s of
    1.65                    SOME s => Var ((s, var_index), T)
    1.66                  | NONE =>
    1.67                    Var ((s |> textual ? repair_variable_name Char.toLower,