author | wenzelm |
Mon, 07 Nov 2016 19:07:30 +0100 | |
changeset 64470 | 85bb70e1260b |
parent 64469 | 488d4e627238 |
child 64471 | c40c2975fb02 |
--- a/src/Pure/theory.ML Mon Nov 07 14:55:39 2016 +0100 +++ b/src/Pure/theory.ML Mon Nov 07 19:07:30 2016 +0100 @@ -220,9 +220,6 @@ fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let - val thy = Proof_Context.theory_of ctxt; - val consts = Sign.consts_of thy; - fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args)