src/Pure/logic.ML
changeset 45344 e209da839ff4
parent 45328 e5b33eecbf6e
child 46215 0da9433f959e
     1.1 --- a/src/Pure/logic.ML	Sat Nov 05 10:59:11 2011 +0100
     1.2 +++ b/src/Pure/logic.ML	Sat Nov 05 15:00:49 2011 +0100
     1.3 @@ -73,6 +73,8 @@
     1.4    val assum_problems: int * term -> (term -> term) * term list * term
     1.5    val varifyT_global: typ -> typ
     1.6    val unvarifyT_global: typ -> typ
     1.7 +  val varify_types_global: term -> term
     1.8 +  val unvarify_types_global: term -> term
     1.9    val varify_global: term -> term
    1.10    val unvarify_global: term -> term
    1.11    val get_goal: term -> int -> term
    1.12 @@ -524,13 +526,20 @@
    1.13  val varifyT_global = Same.commit varifyT_global_same;
    1.14  val unvarifyT_global = Same.commit unvarifyT_global_same;
    1.15  
    1.16 +fun varify_types_global tm = tm
    1.17 +  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
    1.18 +  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.19 +
    1.20 +fun unvarify_types_global tm = tm
    1.21 +  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
    1.22 +  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.23 +
    1.24  fun varify_global tm = tm
    1.25    |> Same.commit (Term_Subst.map_aterms_same
    1.26      (fn Free (x, T) => Var ((x, 0), T)
    1.27        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.28        | _ => raise Same.SAME))
    1.29 -  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
    1.30 -  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.31 +  |> varify_types_global;
    1.32  
    1.33  fun unvarify_global tm = tm
    1.34    |> Same.commit (Term_Subst.map_aterms_same
    1.35 @@ -538,8 +547,7 @@
    1.36        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.37        | Free (x, _) => raise TERM (bad_fixed x, [tm])
    1.38        | _ => raise Same.SAME))
    1.39 -  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
    1.40 -  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.41 +  |> unvarify_types_global;
    1.42  
    1.43  
    1.44  (* goal states *)