--- a/src/Pure/Syntax/syntax_phases.ML Sun Apr 10 23:15:34 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Apr 11 11:48:24 2016 +0200
@@ -970,18 +970,7 @@
end;
-(* standard phases *)
-
-val _ = Context.>>
- (typ_check 0 "standard" Proof_Context.standard_typ_check #>
- term_check 0 "standard"
- (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
- term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
- term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
-
-
-
-(** install operations **)
+(* install operations *)
val _ =
Theory.setup
@@ -1000,3 +989,13 @@
uncheck_terms = uncheck_terms});
end;
+
+
+(* standard phases *)
+
+val _ = Context.>>
+ (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #>
+ Syntax_Phases.term_check 0 "standard"
+ (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
+ Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
+ Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);