src/Pure/Isar/theory_target.ML
changeset 21276 2285cf5a7560
parent 21037 4b52b23f50eb
child 21293 5f5162f40ac7
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Nov 09 21:44:33 2006 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Nov 09 21:44:34 2006 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4        |> LocalTheory.theory_result (fold_map const decls) |>> split_list;
     1.5    in
     1.6      lthy'
     1.7 -    |> K (loc <> "") ? LocalTheory.abbrevs Syntax.default_mode abbrs
     1.8 +    |> K (loc <> "") ? (snd o LocalTheory.abbrevs Syntax.default_mode abbrs)
     1.9      |> LocalDefs.add_defs defns |>> map (apsnd snd)
    1.10    end;
    1.11  
    1.12 @@ -204,22 +204,24 @@
    1.13  
    1.14  (* init and exit *)
    1.15  
    1.16 -fun begin loc =
    1.17 -  Data.put (if loc = "" then NONE else SOME loc) #>
    1.18 -  LocalTheory.init (SOME (NameSpace.base loc))
    1.19 -   {pretty = pretty loc,
    1.20 -    consts = consts loc,
    1.21 -    axioms = axioms,
    1.22 -    defs = defs,
    1.23 -    notes = notes loc,
    1.24 -    term_syntax = term_syntax loc,
    1.25 -    declaration = declaration loc,
    1.26 -    exit = K I};
    1.27 +fun begin loc ctxt = ctxt
    1.28 +  |> Data.put (if loc = "" then NONE else SOME loc)
    1.29 +  |> LocalTheory.init (SOME (NameSpace.base loc))
    1.30 +     {pretty = pretty loc,
    1.31 +      consts = consts loc,
    1.32 +      axioms = axioms,
    1.33 +      defs = defs,
    1.34 +      notes = notes loc,
    1.35 +      term_syntax = term_syntax loc,
    1.36 +      declaration = declaration loc,
    1.37 +      reinit = begin loc,
    1.38 +      exit = K I};
    1.39  
    1.40  fun init_i NONE thy = begin "" (ProofContext.init thy)
    1.41    | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
    1.42  
    1.43 -fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
    1.44 +fun init (SOME "-") thy = init_i NONE thy
    1.45 +  | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
    1.46  
    1.47  fun mapping loc f = init loc #> f #> LocalTheory.exit false;
    1.48