src/Tools/misc_legacy.ML
author blanchet
Mon, 26 Nov 2012 13:35:05 +0100
changeset 50222 40e3c3be6bca
parent 47576 b32aae03e3d6
child 51429 48eb29821bd9
permissions -rw-r--r--
added file headers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/misc_legacy.ML
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     2
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     3
Misc legacy stuff -- to be phased out eventually.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     4
*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     5
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     6
signature MISC_LEGACY =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
     7
sig
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
     8
  val add_term_names: term * string list -> string list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
     9
  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    10
  val add_typ_tfree_names: typ * string list -> string list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    11
  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    12
  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    13
  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    14
  val add_term_tfree_names: term * string list -> string list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    15
  val typ_tfrees: typ -> (string * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    16
  val typ_tvars: typ -> (indexname * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    17
  val term_tfrees: term -> (string * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    18
  val term_tvars: term -> (indexname * sort) list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    19
  val add_term_vars: term * term list -> term list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    20
  val term_vars: term -> term list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    21
  val add_term_frees: term * term list -> term list
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    22
  val term_frees: term -> term list
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    23
  val mk_defpair: term * term -> string * term
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    24
  val get_def: theory -> xstring -> thm
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    25
  val METAHYPS: (thm list -> tactic) -> int -> tactic
47022
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
    26
  val gensym: string -> string
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
    27
  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
    28
  val freeze_thaw: thm -> thm * (thm -> thm)
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    29
end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    30
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    31
structure Misc_Legacy: MISC_LEGACY =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    32
struct
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    33
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    34
(*iterate a function over all types in a term*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    35
fun it_term_types f =
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    36
let fun iter(Const(_,T), a) = f(T,a)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    37
      | iter(Free(_,T), a) = f(T,a)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    38
      | iter(Var(_,T), a) = f(T,a)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    39
      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    40
      | iter(f$u, a) = iter(f, iter(u, a))
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    41
      | iter(Bound _, a) = a
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    42
in iter end
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    43
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    44
(*Accumulates the names in the term, suppressing duplicates.
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    45
  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    46
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    47
  | add_term_names (Free(a,_), bs) = insert (op =) a bs
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    48
  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    49
  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    50
  | add_term_names (_, bs) = bs;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    51
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    52
(*Accumulates the TVars in a type, suppressing duplicates.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    53
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    54
  | add_typ_tvars(TFree(_),vs) = vs
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    55
  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    56
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    57
(*Accumulates the TFrees in a type, suppressing duplicates.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    58
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    59
  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    60
  | add_typ_tfree_names(TVar(_),fs) = fs;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    61
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    62
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    63
  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    64
  | add_typ_tfrees(TVar(_),fs) = fs;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    65
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    66
(*Accumulates the TVars in a term, suppressing duplicates.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    67
val add_term_tvars = it_term_types add_typ_tvars;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    68
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    69
(*Accumulates the TFrees in a term, suppressing duplicates.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    70
val add_term_tfrees = it_term_types add_typ_tfrees;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    71
val add_term_tfree_names = it_term_types add_typ_tfree_names;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    72
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    73
(*Non-list versions*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    74
fun typ_tfrees T = add_typ_tfrees(T,[]);
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    75
fun typ_tvars T = add_typ_tvars(T,[]);
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    76
fun term_tfrees t = add_term_tfrees(t,[]);
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    77
fun term_tvars t = add_term_tvars(t,[]);
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    78
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    79
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    80
(*Accumulates the Vars in the term, suppressing duplicates.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    81
fun add_term_vars (t, vars: term list) = case t of
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    82
    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    83
  | Abs (_,_,body) => add_term_vars(body,vars)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    84
  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    85
  | _ => vars;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    86
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    87
fun term_vars t = add_term_vars(t,[]);
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    88
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    89
(*Accumulates the Frees in the term, suppressing duplicates.*)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    90
fun add_term_frees (t, frees: term list) = case t of
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    91
    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    92
  | Abs (_,_,body) => add_term_frees(body,frees)
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    93
  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    94
  | _ => frees;
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    95
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    96
fun term_frees t = add_term_frees(t,[]);
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    97
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    98
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
    99
fun mk_defpair (lhs, rhs) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   100
  (case Term.head_of lhs of
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   101
    Const (name, _) =>
46909
3c73a121a387 more explicit indication of def names;
wenzelm
parents: 46215
diff changeset
   102
      (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs))
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   103
  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   104
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   105
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   106
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   107
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   108
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   109
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   110
       METAHYPS (fn prems => tac prems) i
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   111
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   112
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   113
proof state A==>A, supplying A1,...,An as meta-level assumptions (in
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   114
"prems").  The parameters x1,...,xm become free variables.  If the
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   115
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   116
then it is lifted back into the original context, yielding k subgoals.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   117
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   118
Replaces unknowns in the context by Frees having the prefix METAHYP_
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   119
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   120
DOES NOT HANDLE TYPE UNKNOWNS.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   121
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   122
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   123
NOTE: This version does not observe the proof context, and thus cannot
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   124
work reliably.  See also Subgoal.SUBPROOF and Subgoal.FOCUS for
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   125
properly localized variants of the same idea.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   126
****)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   127
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   128
local
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   129
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   130
(*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   131
    H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   132
  Main difference from strip_assums concerns parameters:
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   133
    it replaces the bound variables by free variables.  *)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   134
fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   135
      strip_context_aux (params, H :: Hs, B)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   136
  | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 39288
diff changeset
   137
      let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   138
      in strip_context_aux ((b, T) :: params, Hs, u) end
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   139
  | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   140
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   141
fun strip_context A = strip_context_aux ([], [], A);
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   142
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   143
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   144
  Instantiates distinct free variables by terms of same type.*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   145
fun free_instantiate ctpairs =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   146
  forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   147
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   148
fun free_of s ((a, i), T) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   149
  Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   150
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   151
fun mk_inst v = (Var v, free_of "METAHYP1_" v)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   152
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   153
fun metahyps_split_prem prem =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   154
  let (*find all vars in the hyps -- should find tvars also!*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   155
      val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   156
      val insts = map mk_inst hyps_vars
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   157
      (*replace the hyps_vars by Frees*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   158
      val prem' = subst_atomic insts prem
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   159
      val (params,hyps,concl) = strip_context prem'
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   160
  in (insts,params,hyps,concl)  end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   161
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   162
fun metahyps_aux_tac tacf (prem,gno) state =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   163
  let val (insts,params,hyps,concl) = metahyps_split_prem prem
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   164
      val maxidx = Thm.maxidx_of state
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   165
      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   166
      val chyps = map cterm hyps
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   167
      val hypths = map Thm.assume chyps
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   168
      val subprems = map (Thm.forall_elim_vars 0) hypths
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   169
      val fparams = map Free params
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   170
      val cparams = map cterm fparams
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   171
      fun swap_ctpair (t,u) = (cterm u, cterm t)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   172
      (*Subgoal variables: make Free; lift type over params*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   173
      fun mk_subgoal_inst concl_vars (v, T) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   174
          if member (op =) concl_vars (v, T)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   175
          then ((v, T), true, free_of "METAHYP2_" (v, T))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   176
          else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   177
      (*Instantiate subgoal vars by Free applied to params*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   178
      fun mk_ctpair (v, in_concl, u) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   179
          if in_concl then (cterm (Var v), cterm u)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   180
          else (cterm (Var v), cterm (list_comb (u, fparams)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   181
      (*Restore Vars with higher type and index*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   182
      fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   183
          if in_concl then (cterm u, cterm (Var ((a, i), T)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   184
          else (cterm u, cterm (Var ((a, i + maxidx), U)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   185
      (*Embed B in the original context of params and hyps*)
46215
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 45862
diff changeset
   186
      fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   187
      (*Strip the context using elimination rules*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   188
      fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   189
      (*A form of lifting that discharges assumptions.*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   190
      fun relift st =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   191
        let val prop = Thm.prop_of st
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   192
            val subgoal_vars = (*Vars introduced in the subgoals*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   193
              fold Term.add_vars (Logic.strip_imp_prems prop) []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   194
            and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   195
            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   196
            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   197
            val emBs = map (cterm o embed) (prems_of st')
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   198
            val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   199
        in  (*restore the unknowns to the hypotheses*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   200
            free_instantiate (map swap_ctpair insts @
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   201
                              map mk_subgoal_swap_ctpair subgoal_insts)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   202
                (*discharge assumptions from state in same order*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   203
                (implies_intr_list emBs
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   204
                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   205
        end
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   206
      (*function to replace the current subgoal*)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   207
      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   208
  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   209
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   210
fun print_vars_terms n thm =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   211
  let
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   212
    val thy = theory_of_thm thm
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   213
    fun typed s ty =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   214
      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   215
    fun find_vars (Const (c, ty)) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   216
          if null (Term.add_tvarsT ty []) then I
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   217
          else insert (op =) (typed c ty)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   218
      | find_vars (Var (xi, ty)) =
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   219
          insert (op =) (typed (Term.string_of_vname xi) ty)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   220
      | find_vars (Free _) = I
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   221
      | find_vars (Bound _) = I
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   222
      | find_vars (Abs (_, _, t)) = find_vars t
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   223
      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   224
    val prem = Logic.nth_prem (n, Thm.prop_of thm)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   225
    val tms = find_vars prem []
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   226
  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   227
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   228
in
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   229
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   230
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   231
  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   232
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   233
end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   234
47022
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   235
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   236
(* generating identifiers -- often fresh *)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   237
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   238
local
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   239
(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   240
fun gensym_char i =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   241
  if i<26 then chr (ord "A" + i)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   242
  else if i<52 then chr (ord "a" + i - 26)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   243
  else chr (ord "0" + i - 52);
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   244
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   245
val char_vec = Vector.tabulate (62, gensym_char);
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   246
fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   247
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   248
val gensym_seed = Unsynchronized.ref (0: int);
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   249
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   250
in
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   251
  fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   252
end;
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
diff changeset
   253
47022
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   254
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   255
(*Convert all Vars in a theorem to Frees.  Also return a function for
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   256
  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   257
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   258
fun freeze_thaw_robust th =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   259
 let val fth = Thm.legacy_freezeT th
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   260
     val thy = Thm.theory_of_thm fth
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   261
 in
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   262
   case Thm.fold_terms Term.add_vars fth [] of
47576
b32aae03e3d6 dropped dead code;
haftmann
parents: 47022
diff changeset
   263
       [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
47022
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   264
     | vars =>
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   265
         let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   266
             val alist = map newName vars
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   267
             fun mk_inst (v,T) =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   268
                 (cterm_of thy (Var(v,T)),
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   269
                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   270
             val insts = map mk_inst vars
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   271
             fun thaw i th' = (*i is non-negative increment for Var indexes*)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   272
                 th' |> forall_intr_list (map #2 insts)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   273
                     |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   274
         in  (Thm.instantiate ([],insts) fth, thaw)  end
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   275
 end;
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   276
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   277
(*Basic version of the function above. No option to rename Vars apart in thaw.
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   278
  The Frees created from Vars have nice names.*)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   279
fun freeze_thaw th =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   280
 let val fth = Thm.legacy_freezeT th
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   281
     val thy = Thm.theory_of_thm fth
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   282
 in
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   283
   case Thm.fold_terms Term.add_vars fth [] of
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   284
       [] => (fth, fn x => x)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   285
     | vars =>
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   286
         let fun newName (ix, _) (pairs, used) =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   287
                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   288
                   in  ((ix,v)::pairs, v::used)  end;
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   289
             val (alist, _) =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   290
                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   291
             fun mk_inst (v, T) =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   292
                 (cterm_of thy (Var(v,T)),
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   293
                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   294
             val insts = map mk_inst vars
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   295
             fun thaw th' =
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   296
                 th' |> forall_intr_list (map #2 insts)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   297
                     |> forall_elim_list (map #1 insts)
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   298
         in  (Thm.instantiate ([],insts) fth, thaw)  end
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   299
 end;
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   300
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   301
end;
8eac39af4ec0 moved some legacy stuff;
wenzelm
parents: 46909
diff changeset
   302