src/Pure/Isar/expression.ML
changeset 30776 fcd49e932503
parent 30774 5daee9354a9c
child 30777 9960ff945c52
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:47:50 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 17:47:58 2009 +0200
     1.3 @@ -173,8 +173,8 @@
     1.4      (* instantiation *)
     1.5      val (type_parms'', res') = chop (length type_parms) res;
     1.6      val insts'' = (parm_names ~~ res') |> map_filter
     1.7 -      (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
     1.8 -        inst => SOME inst);
     1.9 +      (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
    1.10 +        | inst => SOME inst);
    1.11      val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
    1.12      val inst = Symtab.make insts'';
    1.13    in
    1.14 @@ -242,7 +242,7 @@
    1.15        in
    1.16          ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
    1.17            (ctxt', ts))
    1.18 -      end
    1.19 +      end;
    1.20      val (cs', (context', _)) = fold_map prep cs
    1.21        (context, Syntax.check_terms
    1.22          (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
    1.23 @@ -260,7 +260,8 @@
    1.24        (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
    1.25      val (elem_css', [concl_cs']) = chop (length elem_css) css';
    1.26    in
    1.27 -    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
    1.28 +    (map restore_inst (insts ~~ inst_cs'),
    1.29 +      map restore_elem (elems ~~ elem_css'),
    1.30        concl_cs', ctxt')
    1.31    end;
    1.32  
    1.33 @@ -278,6 +279,7 @@
    1.34    | declare_elem _ (Defines _) ctxt = ctxt
    1.35    | declare_elem _ (Notes _) ctxt = ctxt;
    1.36  
    1.37 +
    1.38  (** Finish locale elements **)
    1.39  
    1.40  fun closeup _ _ false elem = elem
    1.41 @@ -392,9 +394,11 @@
    1.42  fun cert_full_context_statement x =
    1.43    prep_full_context_statement (K I) (K I) ProofContext.cert_vars
    1.44    make_inst ProofContext.cert_vars (K I) x;
    1.45 +
    1.46  fun cert_read_full_context_statement x =
    1.47    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
    1.48    make_inst ProofContext.cert_vars (K I) x;
    1.49 +
    1.50  fun read_full_context_statement x =
    1.51    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
    1.52    parse_inst ProofContext.read_vars intern x;
    1.53 @@ -727,7 +731,8 @@
    1.54      val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
    1.55      val _ =
    1.56        if null extraTs then ()
    1.57 -      else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
    1.58 +      else warning ("Additional type variable(s) in locale specification " ^
    1.59 +        quote (Binding.str_of bname));
    1.60  
    1.61      val a_satisfy = Element.satisfy_morphism a_axioms;
    1.62      val b_satisfy = Element.satisfy_morphism b_axioms;