src/Pure/logic.ML
changeset 31981 9c59cbb9c5a2
parent 31943 5e960a0780a2
child 32004 6ef7056e5215
     1.1 --- a/src/Pure/logic.ML	Fri Jul 10 00:08:38 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Fri Jul 10 00:47:17 2009 +0200
     1.3 @@ -476,30 +476,35 @@
     1.4  fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
     1.5  fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
     1.6  
     1.7 -fun varifyT ty = ty |> Term.map_atyps
     1.8 -  (fn TFree (a, S) => TVar ((a, 0), S)
     1.9 -    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
    1.10 +fun varifyT_option ty = ty
    1.11 +  |> Term_Subst.map_atypsT_option
    1.12 +    (fn TFree (a, S) => SOME (TVar ((a, 0), S))
    1.13 +      | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
    1.14  
    1.15 -fun unvarifyT ty = ty |> Term.map_atyps
    1.16 -  (fn TVar ((a, 0), S) => TFree (a, S)
    1.17 -    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
    1.18 -    | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
    1.19 +fun unvarifyT_option ty = ty
    1.20 +  |> Term_Subst.map_atypsT_option
    1.21 +    (fn TVar ((a, 0), S) => SOME (TFree (a, S))
    1.22 +      | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
    1.23 +      | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
    1.24  
    1.25 -fun varify tm =
    1.26 -  tm |> Term.map_aterms
    1.27 -    (fn Free (x, T) => Var ((x, 0), T)
    1.28 +val varifyT = perhaps varifyT_option;
    1.29 +val unvarifyT = perhaps unvarifyT_option;
    1.30 +
    1.31 +fun varify tm = tm
    1.32 +  |> perhaps (Term_Subst.map_aterms_option
    1.33 +    (fn Free (x, T) => SOME (Var ((x, 0), T))
    1.34        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.35 -      | t => t)
    1.36 -  |> Term.map_types varifyT
    1.37 +      | _ => NONE))
    1.38 +  |> perhaps (Term_Subst.map_types_option varifyT_option)
    1.39    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.40  
    1.41 -fun unvarify tm =
    1.42 -  tm |> Term.map_aterms
    1.43 -    (fn Var ((x, 0), T) => Free (x, T)
    1.44 +fun unvarify tm = tm
    1.45 +  |> perhaps (Term_Subst.map_aterms_option
    1.46 +    (fn Var ((x, 0), T) => SOME (Free (x, T))
    1.47        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.48        | Free (x, _) => raise TERM (bad_fixed x, [tm])
    1.49 -      | t => t)
    1.50 -  |> Term.map_types unvarifyT
    1.51 +      | _ => NONE))
    1.52 +  |> perhaps (Term_Subst.map_types_option unvarifyT_option)
    1.53    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.54  
    1.55  val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);