equal
deleted
inserted
replaced
241 let |
241 let |
242 val fs = fold_rev (fn eq => |
242 val fs = fold_rev (fn eq => |
243 insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop |
243 insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop |
244 |> HOLogic.dest_eq |> fst |> strip_comb |
244 |> HOLogic.dest_eq |> fst |> strip_comb |
245 |> fst)) raw_eqs [] |
245 |> fst)) raw_eqs [] |
246 val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl) |
246 val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl) |
247 union ts) fs [] |
247 ) fs [] |
248 val _ = bds := AList.make (fn _ => ([],[])) tys |
248 val _ = bds := AList.make (fn _ => ([],[])) tys |
249 val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt |
249 val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt |
250 val thy = ProofContext.theory_of ctxt' |
250 val thy = ProofContext.theory_of ctxt' |
251 val cert = cterm_of thy |
251 val cert = cterm_of thy |
252 val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) |
252 val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) |