changeset 42361 | 23f352990944 |
parent 42151 | 4da4fc77664b |
child 42375 | 774df7c59508 |
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Sat Apr 16 16:15:37 2011 +0200 @@ -193,7 +193,7 @@ (* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *) fun read_typ thy sorts str = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy |> fold (Variable.declare_typ o TFree) sorts in Syntax.read_typ ctxt str end